Documentation Verification Report

Factorization

📁 Source: Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean

Statistics

Metric	Count
Definitions	0
Theorems `irreducible_of_dvd_cyclotomic_of_natDegree`, `natDegree_of_dvd_cyclotomic_of_irreducible`, `natDegree_of_mem_normalizedFactors_cyclotomic`, `normalizedFactors_cyclotomic_card`, `irreducible_of_dvd_cyclotomic_of_natDegree`	5
Total	5

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_of_dvd_cyclotomic_of_natDegree` 📖	mathematical	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing` `natDegree` `orderOf` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Units.instMonoid` `ZMod.unitOfCoprime`	`Irreducible` `semiring`	—	`ne_zero_of_dvd_ne_zero` `cyclotomic_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `UniqueFactorizationMonoid.exists_mem_normalizedFactors` `not_isUnit_of_natDegree_pos` `pos_of_ne_zero` `Nat.instCanonicallyOrderedAdd` `orderOf_eq_zero_iff` `isOfFinOrder_of_finite` `instFiniteZModUnits` `Associated.irreducible` `associated_of_dvd_of_natDegree_le` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `natDegree_of_dvd_cyclotomic_of_irreducible` `Multiset.mem_of_le` `UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors` `UniqueFactorizationMonoid.irreducible_of_normalized_factor` `le_refl`
`natDegree_of_dvd_cyclotomic_of_irreducible` 📖	mathematical	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing` `Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	`natDegree` `orderOf` `Units` `ZMod` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Units.instMonoid` `ZMod.unitOfCoprime`	—	`inv_mul_cancel₀` `leadingCoeff_ne_zero` `Irreducible.ne_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `natDegree_mul_leadingCoeff_self_inv` `irreducible_mul_leadingCoeff_inv` `monic_mul_leadingCoeff_inv`
`natDegree_of_mem_normalizedFactors_cyclotomic` 📖	mathematical	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Multiset` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `Multiset.instMembership` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `commSemiring` `Semifield.toCommSemiring` `instNormalizationMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDomain.to_noZeroDivisors` `instIsDomain` `NormalizedGCDMonoid.toNormalizationMonoid` `CommRing.toCommSemiring` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `instIsSimpleModule` `cyclotomic`	`natDegree` `orderOf` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ZMod.commRing` `Units.instMonoid` `ZMod.unitOfCoprime`	—	`IsDomain.to_noZeroDivisors` `instIsDomain` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `natDegree_of_dvd_cyclotomic_of_irreducible` `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors` `UniqueFactorizationMonoid.irreducible_of_normalized_factor`
`normalizedFactors_cyclotomic_card` 📖	mathematical	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid`	`Finset.card` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `Multiset.toFinset` `instDecidableEq` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `commSemiring` `Semifield.toCommSemiring` `instNormalizationMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDomain.to_noZeroDivisors` `instIsDomain` `NormalizedGCDMonoid.toNormalizationMonoid` `CommRing.toCommSemiring` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `Ring.toAddCommGroup` `Semiring.toModule` `instIsSimpleModule` `cyclotomic` `Nat.totient` `orderOf` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ZMod.commRing` `Units.instMonoid` `ZMod.unitOfCoprime`	—	`IsDomain.to_noZeroDivisors` `instIsDomain` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsPrincipalIdealRingOfIsSemisimpleRing` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `UniqueFactorizationMonoid.prod_normalizedFactors` `cyclotomic_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `natDegree_of_mem_normalizedFactors_cyclotomic` `natDegree_eq_of_degree_eq` `degree_eq_degree_of_associated` `Multiset.map_const'` `Multiset.sum_replicate` `Multiset.map_congr` `natDegree_multiset_prod` `UniqueFactorizationMonoid.zero_notMem_normalizedFactors` `natDegree_cyclotomic` `orderOf_pos` `instFiniteZModUnits` `Multiset.toFinset_card_of_nodup` `Multiset.nodup_iff_count_le_one` `charP_of_card_eq_prime_pow` `Nat.Prime.coprime_iff_not_dvd` `Fact.out` `Nat.coprime_pow_left_iff` `pos_of_ne_zero` `Nat.instCanonicallyOrderedAdd` `CharP.cast_eq_zero_iff` `Multiset.count_pos` `Prime.not_unit` `UniqueFactorizationMonoid.prime_of_normalized_factor` `squarefree_cyclotomic` `Multiset.le_iff_count` `Multiset.count.congr_simp` `Multiset.count_cons_self` `Multiset.count_eq_one_of_mem` `Multiset.count_eq_zero_of_notMem` `Multiset.prod_dvd_prod_of_le` `Dvd.dvd.trans` `Multiset.prod_cons` `Multiset.prod_singleton` `Associated.dvd`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_of_dvd_cyclotomic_of_natDegree` 📖	mathematical	`Polynomial` `ZMod` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `commRing` `Polynomial.cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.natDegree` `orderOf` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.instMonoid` `unitOfCoprime` `Nat.Prime.coprime_iff_not_dvd` `Fact.out` `Nat.Prime`	`Irreducible` `Polynomial.semiring`	—	`Nat.Prime.coprime_iff_not_dvd` `Fact.out` `Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `card` `pow_one` `unitOfCoprime.congr_simp`

---

← Back to Index