FormalConjecturesForMathlib/Algebra/Polynomial/Algebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Algebra over the Ring of Polynomials

Imports (2)
Imported by 1 file
  1. instance Polynomial.instAlgebraPi line 33 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommSemiring, Algebra, Polynomial

    Proof uses: RingHom.toAlgebra, RingHom.pi, AlgHom.toRingHom, Polynomial.aeval

    10 instances, coercions and auxiliary constants left out.

  2. lemma Polynomial.algebraMap_algebraPi line 37 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommSemiring, Algebra, Polynomial, Eq, RingHom, Algebra.algebraMap, AlgHom, Polynomial.aeval

    Proof uses: rfl

    18 instances, coercions and auxiliary constants left out.

  3. lemma Polynomial.aeval_polynomial_pi line 39 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommSemiring, Algebra, Polynomial, Eq, AlgHom, Polynomial.aeval, Polynomial.aevalAeval

    Proof uses: Polynomial.induction_on', of_eq_true, HAdd.hAdd, Eq.trans, Polynomial.eval, Polynomial.algebra, RingHom, Polynomial.C, True, congr, congrArg, congrFun, map_add, RingHom.id, Prod.fst, Prod.mk, Prod.snd, Polynomial.aevalAevalEquiv_apply_apply, Equiv, Prod and 19 more

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.