Monomial

Statistics

Metric	Count
Definitions	0
Theorems `C_mul_X_pow_eq_self`, `monomial_natDegree_leadingCoeff_eq_self`, `natDegree_le_pred`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mul_X_pow_eq_self` 📖	mathematical	`Finset.card` `support`	`Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `natDegree`	—	`C_mul_X_pow_eq_monomial` `monomial_natDegree_leadingCoeff_eq_self`
`monomial_natDegree_leadingCoeff_eq_self` 📖	mathematical	`Finset.card` `support`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `natDegree` `leadingCoeff`	—	`card_support_le_one_iff_monomial` `monomial_zero_right` `natDegree_monomial` `leadingCoeff_monomial`
`natDegree_le_pred` 📖	—	`natDegree` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—	`Nat.le_succ_iff_eq_or_le` `leadingCoeff_eq_zero` `coeff_natDegree`

---