Documentation Verification Report

KummerPolynomial

📁 Source: Mathlib/FieldTheory/KummerPolynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems `X_pow_sub_C_irreducible_iff_of_prime`, `X_pow_sub_C_irreducible_of_prime`, `ne_zero_of_irreducible_X_pow_sub_C`, `ne_zero_of_irreducible_X_pow_sub_C'`, `pow_ne_of_irreducible_X_pow_sub_C`, `root_X_pow_sub_C_eq_zero_iff`, `root_X_pow_sub_C_ne_zero`, `root_X_pow_sub_C_ne_zero'`, `root_X_pow_sub_C_ne_zero_iff`, `root_X_pow_sub_C_pow`	10
Total	10

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_pow_sub_C_irreducible_iff_of_prime` 📖	mathematical	`Nat.Prime`	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`pow_ne_of_irreducible_X_pow_sub_C` `dvd_rfl` `Nat.Prime.ne_one` `X_pow_sub_C_irreducible_of_prime`
`X_pow_sub_C_irreducible_of_prime` 📖	mathematical	`Nat.Prime`	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`Polynomial.isUnit_iff_degree_eq_zero` `Polynomial.degree_X_pow_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.Prime.pos` `Nat.cast_eq_zero` `WithBot.charZero` `Nat.instCharZero` `Nat.Prime.ne_zero` `WfDvdMonoid.exists_irreducible_factor` `UniqueFactorizationMonoid.toIsWellFounded` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.X_pow_sub_C_ne_zero` `Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero` `AdjoinRoot.eval₂_root` `map_pow` `MonoidHom.instMonoidHomClass` `sub_eq_zero` `Polynomial.eval₂_X` `Polynomial.eval₂_C` `Polynomial.eval₂_pow` `Polynomial.eval₂_sub` `AdjoinRoot.algebraMap_eq` `Algebra.norm_algebraMap` `Irreducible.ne_zero` `PowerBasis.finrank` `commRing_strongRankCondition` `AdjoinRoot.powerBasis_dim` `Nat.Prime.coprime_iff_not_dvd` `LE.le.antisymm` `LE.le.trans_eq` `Polynomial.natDegree_le_of_dvd` `IsDomain.to_noZeroDivisors` `Polynomial.natDegree_X_pow_sub_C` `Polynomial.natDegree_pos_iff_degree_pos` `Polynomial.degree_pos_of_irreducible` `pow_mem_range_pow_of_coprime` `Associated.irreducible` `Polynomial.associated_of_dvd_of_natDegree_le` `Eq.ge`
`ne_zero_of_irreducible_X_pow_sub_C` 📖	—	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	—	`Polynomial.not_irreducible_C` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `RingHom.map_one` `pow_zero`
`ne_zero_of_irreducible_X_pow_sub_C'` 📖	—	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	—	`not_irreducible_pow` `sub_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`pow_ne_of_irreducible_X_pow_sub_C` 📖	—	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	—	`Polynomial.not_irreducible_C` `pow_zero` `RingHom.map_one` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_dvd_pow_sub_pow` `Polynomial.degree_X_pow_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `mul_ne_zero_iff` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `WithBot.charZero` `Nat.instCharZero` `Irreducible.isUnit_or_isUnit` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_mul` `mul_comm` `mul_eq_right₀` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `Polynomial.degree_mul` `IsDomain.to_noZeroDivisors` `instIsDomain` `add_zero` `Nat.cast_injective`
`root_X_pow_sub_C_eq_zero_iff` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	`AdjoinRoot.root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AdjoinRoot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AdjoinRoot.instCommRing`	—	`ne_zero_of_irreducible_X_pow_sub_C` `not_imp_not` `root_X_pow_sub_C_ne_zero'` `ne_zero_of_irreducible_X_pow_sub_C'` `pow_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_zero` `AdjoinRoot.mk_X` `AdjoinRoot.mk_self`
`root_X_pow_sub_C_ne_zero` 📖	—	—	—	—	`AdjoinRoot.mk_ne_zero_of_natDegree_lt` `Polynomial.monic_X_pow_sub_C` `Polynomial.X_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.natDegree_X_pow_sub_C` `Polynomial.natDegree_X`
`root_X_pow_sub_C_ne_zero'` 📖	—	—	—	—	`LE.le.eq_or_lt` `pow_one` `AdjoinRoot.mk_ne_zero_of_natDegree_lt` `Polynomial.monic_X_sub_C` `Polynomial.C_ne_zero` `Polynomial.natDegree_C` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_X` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.instZeroLEOneClass` `sub_sub_cancel` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `AdjoinRoot.mk_self` `sub_zero` `AdjoinRoot.mk_X` `root_X_pow_sub_C_ne_zero`
`root_X_pow_sub_C_ne_zero_iff` 📖	—	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	—	`Iff.not` `root_X_pow_sub_C_eq_zero_iff`
`root_X_pow_sub_C_pow` 📖	mathematical	—	`AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `AdjoinRoot.instCommRing` `AdjoinRoot.root` `AdjoinRoot.of`	—	`sub_eq_zero` `AdjoinRoot.eval₂_root` `Polynomial.eval₂_sub` `Polynomial.eval₂_C` `Polynomial.eval₂_pow` `Polynomial.eval₂_X`

---

← Back to Index