Documentation Verification Report

UniqueFactorization

📁 Source: Mathlib/RingTheory/Polynomial/UniqueFactorization.lean

Statistics

Metric	Count
Definitions `fintypeSubtypeMonicDvd`	1
Theorems `uniqueFactorizationMonoid`, `exists_irreducible_of_degree_pos`, `exists_irreducible_of_natDegree_ne_zero`, `exists_irreducible_of_natDegree_pos`, `exists_monic_irreducible_factor`, `uniqueFactorizationMonoid`, `wfDvdMonoid`	7
Total	8

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueFactorizationMonoid` 📖	mathematical	—	`UniqueFactorizationMonoid` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring`	—	`UniqueFactorizationMonoid.iff_exists_prime_factors` `instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `UniqueFactorizationMonoid.toIsCancelMulZero` `exists_finset_rename` `Finite.of_fintype` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Multiset.mem_map` `prime_rename_iff` `Multiset.prod_hom` `MonoidWithZeroHomClass.toMonoidHomClass` `Units.coe_map` `AlgHom.toRingHom_eq_coe` `RingHom.instRingHomClass` `RingHom.toMonoidHom_eq_coe` `AlgHom.toRingHom_toMonoidHom` `MonoidHom.coe_coe` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass`

Polynomial

Definitions

Name	Category	Theorems
`fintypeSubtypeMonicDvd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_irreducible_of_degree_pos` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `CommSemiring.toSemiring`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	—	`WfDvdMonoid.exists_irreducible_factor` `wfDvdMonoid` `ne_of_gt` `degree_eq_zero_of_isUnit` `not_lt_of_gt` `WithBot.bot_lt_coe` `degree_zero`
`exists_irreducible_of_natDegree_ne_zero` 📖	mathematical	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	—	`exists_irreducible_of_natDegree_pos`
`exists_irreducible_of_natDegree_pos` 📖	mathematical	`natDegree` `CommSemiring.toSemiring`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	—	`exists_irreducible_of_degree_pos` `Mathlib.Tactic.Contrapose.contrapose₁` `natDegree_le_of_degree_le`
`exists_monic_irreducible_factor` 📖	mathematical	`IsUnit` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	`Monic` `Irreducible` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`monic_X` `irreducible_X` `instIsDomain` `dvd_zero` `WfDvdMonoid.exists_irreducible_factor` `UniqueFactorizationMonoid.toIsWellFounded` `uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `EuclideanDomain.to_principal_ideal_domain` `associated_mul_unit_right` `isUnit_C` `IsUnit.inv` `Ne.isUnit` `leadingCoeff_ne_zero` `Irreducible.ne_zero` `monic_mul_leadingCoeff_inv` `Associated.irreducible` `Associated.dvd_iff_dvd_left`
`uniqueFactorizationMonoid` 📖	mathematical	—	`UniqueFactorizationMonoid` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring`	—	`ufm_of_decomposition_of_wfDvdMonoid` `instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `UniqueFactorizationMonoid.toIsCancelMulZero` `UniqueFactorizationMonoid.toIsWellFounded` `wfDvdMonoid` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `instDecompositionMonoidOfNonemptyGCDMonoid` `instNonemptyGCDMonoidOfNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid`
`wfDvdMonoid` 📖	mathematical	—	`WfDvdMonoid` `Polynomial` `CommSemiring.toSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring`	—	`RelHomClass.wellFounded` `RelHom.instRelHomClass` `degree_mul` `leadingCoeff_zero` `WithTop.coe_lt_top` `right_ne_zero_of_mul` `leadingCoeff_mul` `Nat.cast_zero` `add_zero` `leadingCoeff_eq_zero` `isUnit_iff` `eq_C_of_degree_eq_zero` `leadingCoeff.eq_1` `natDegree_eq_of_degree_eq_some` `degree_eq_natDegree` `WithTop.coe_lt_coe` `Nat.cast_add` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `WellFounded.prod_lex` `wellFounded_lt` `WithTop.instWellFoundedLT` `WithBot.instWellFoundedLT` `instWellFoundedLTNat` `IsWellFounded.wf`

---

← Back to Index