Algebra

Statistics

Metric	Count
Definitions	0
Theorems `eval₂_comp'`, `eval₂_mul'`, `eval₂_pow'`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`eval₂_comp'` 📖	mathematical	—	`eval₂` `CommSemiring.toSemiring` `algebraMap` `comp`	—	`induction_on'` `add_comp` `eval₂_add` `monomial_comp` `eval₂_mul'` `eval₂_C` `eval₂_pow'` `eval₂_monomial`
`eval₂_mul'` 📖	mathematical	—	`eval₂` `CommSemiring.toSemiring` `algebraMap` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eval₂_mul_noncomm` `Algebra.commute_algebraMap_left`
`eval₂_pow'` 📖	mathematical	—	`eval₂` `CommSemiring.toSemiring` `algebraMap` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`pow_zero` `eval₂_one` `pow_succ` `eval₂_mul'`

---