Polynomial

Statistics

Metric	Count
Definitions	0
Theorems `eval_polynomial_eval_finSuccEquiv`, `polynomial_eval_eval₂`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_polynomial_eval_finSuccEquiv` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval` `Polynomial.eval` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `AlgEquiv` `Polynomial` `Polynomial.semiring` `AddMonoidAlgebra.algebra` `Algebra.id` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `finSuccEquiv`	—	`finSuccEquiv_apply` `polynomial_eval_eval₂` `eval_eval₂` `RingHom.ext` `Polynomial.eval_C` `eval_C` `Polynomial.eval_X` `eval_X`
`polynomial_eval_eval₂` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `eval₂` `Polynomial` `Polynomial.commSemiring` `RingHom.comp` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Polynomial.evalRingHom`	—	`induction_on` `eval₂_C` `eval₂_add` `Polynomial.eval_add` `eval₂_mul` `eval₂_X` `Polynomial.eval_mul`

---