Minpoly

Statistics

Metric	Count
Definitions	0
Theorems `coeff_zero_minpoly`, `pow_coeff_zero_ne_zero_of_unit`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_zero_minpoly` 📖	mathematical	—	`DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `instFunLike` `Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `RingHom` `Semiring.toNonAssocSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap`	—	`minpoly.eq_X_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.coeff_sub` `Polynomial.coeff_X_zero` `Polynomial.coeff_C_zero` `zero_sub` `map_neg`
`pow_coeff_zero_ne_zero_of_unit` 📖	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	—	`Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsAlgebraic.isIntegral` `Algebra.IsAlgebraic.isAlgebraic` `minpoly.natDegree_le` `minpoly.natDegree_pos` `pow_eq_zero_iff` `isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors` `LT.lt.ne` `zero_iff` `GroupWithZero.toNontrivial` `minpoly.coeff_zero_ne_zero` `instIsDomain` `IsUnit.ne_zero`

---