Basic

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `card_factors_eq`, `prod_le_prod_iff_le`, `ufm`, `unique'`, `uniqueFactorizationMonoid`, `uniqueFactorizationMonoid_iff`, `dvd_of_dvd_mul_left_of_no_prime_factors`, `dvd_of_dvd_mul_right_of_no_prime_factors`, `exists_mem_factors`, `exists_mem_factors_of_dvd`, `exists_reduced_factors`, `exists_reduced_factors'`, `factors_eq_singleton_of_irreducible`, `factors_eq_zero`, `factors_mul`, `factors_of_isUnit`, `factors_one`, `factors_pos`, `factors_pow`, `factors_pow_count_prod`, `factors_rel_of_associated`, `factors_unique`, `iff_exists_prime_factors`, `isRelPrime_iff_no_prime_factors`, `of_existsUnique_irreducible_factors`, `of_exists_prime_factors`, `iff_wellFounded_associates`, `of_exists_prime_factors`, `of_wellFoundedLT_associates`, `of_wfDvdMonoid_associates`, `wellFoundedLT_associates`, `wfDvdMonoid_associates`, `irreducible_iff_prime_of_existsUnique_irreducible_factors`, `irreducible_iff_prime_of_exists_prime_factors`, `prime_factors_irreducible`, `prime_factors_unique`	36
Total	36

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_factors_eq` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Multiset.card` `UniqueFactorizationMonoid.factors`	—	`UniqueFactorizationMonoid.factors.congr_simp` `UniqueFactorizationMonoid.factors_zero` `ne_zero_iff` `Multiset.card_eq_card_of_rel` `UniqueFactorizationMonoid.factors_unique` `UniqueFactorizationMonoid.irreducible_of_factor` `trans` `UniqueFactorizationMonoid.factors_prod` `symm`

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_le_prod_iff_le` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid` `Multiset.prod` `instCommMonoid` `Multiset` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	—	`Multiset.le_iff_exists_add` `ufm` `unique'` `Multiset.mem_add` `UniqueFactorizationMonoid.irreducible_of_factor` `Multiset.prod_add` `associated_iff_eq` `Unique.instSubsingleton` `Associated.symm` `UniqueFactorizationMonoid.factors_prod` `not_irreducible_zero` `Multiset.prod_eq_zero_iff` `instNoZeroDivisors` `UniqueFactorizationMonoid.toIsCancelMulZero` `instNontrivial` `MulZeroClass.mul_zero` `prod_le_prod`
`ufm` 📖	mathematical	—	`UniqueFactorizationMonoid` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	—	`WfDvdMonoid.wfDvdMonoid_associates` `UniqueFactorizationMonoid.toIsWellFounded` `instIsCancelMulZero` `UniqueFactorizationMonoid.toIsCancelMulZero` `irreducible_iff_prime_iff` `UniqueFactorizationMonoid.irreducible_iff_prime`
`unique'` 📖	—	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Multiset.prod` `instCommMonoid` `CommMonoidWithZero.toCommMonoid`	—	—	`Multiset.induction_on_multiset_quot` `Multiset.map_mk_eq_map_mk_of_rel` `UniqueFactorizationMonoid.factors_unique` `Multiset.mem_map_of_mem` `mk_eq_mk_iff_associated`

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueFactorizationMonoid` 📖	mathematical	—	`UniqueFactorizationMonoid`	—	`isCancelMulZero_iff` `UniqueFactorizationMonoid.toIsCancelMulZero` `UniqueFactorizationMonoid.iff_exists_prime_factors` `apply_symm_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MulEquivClass.toMonoidWithZeroHomClass` `instMulEquivClass` `Multiset.mem_map` `prime_iff` `Multiset.prod_hom` `MonoidWithZeroHomClass.toMonoidHomClass` `MulEquivClass.instMonoidHomClass` `toMonoidHom_eq_coe` `Units.coe_map` `MonoidHom.coe_coe` `map_mul` `MonoidHomClass.toMulHomClass`
`uniqueFactorizationMonoid_iff` 📖	mathematical	—	`UniqueFactorizationMonoid`	—	`uniqueFactorizationMonoid`

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_dvd_mul_left_of_no_prime_factors` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`IsRelPrime.dvd_of_dvd_mul_right` `instDecompositionMonoid` `isRelPrime_iff_no_prime_factors`
`dvd_of_dvd_mul_right_of_no_prime_factors` 📖	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—	`mul_comm` `dvd_of_dvd_mul_left_of_no_prime_factors`
`exists_mem_factors` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Multiset` `Multiset.instMembership` `factors`	—	`WfDvdMonoid.exists_irreducible_factor` `toIsWellFounded` `exists_mem_factors_of_dvd`
`exists_mem_factors_of_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`Multiset` `Multiset.instMembership` `factors` `Associated`	—	`MulZeroClass.mul_zero` `factors_unique` `Multiset.mem_cons` `irreducible_of_factor` `Associated.symm` `Associated.instIsTrans` `factors_prod` `Multiset.prod_cons` `Associated.mul_left` `Multiset.exists_mem_of_rel_of_mem`
`exists_reduced_factors` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`induction_on_prime` `isUnit_of_dvd_unit` `one_mul` `mul_assoc` `Prime.left_dvd_or_dvd_right_of_dvd_mul` `toIsCancelMulZero` `dvd_mul_of_dvd_right` `Dvd.dvd.trans` `mul_left_comm`
`exists_reduced_factors'` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`exists_reduced_factors`
`factors_eq_singleton_of_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Associated` `factors` `Multiset` `Multiset.instSingleton`	—	`exists_mem_factors_of_dvd` `Irreducible.ne_zero` `dvd_rfl` `Multiset.eq_of_le_of_card_le` `Multiset.singleton_le` `card_factors_of_irreducible` `Multiset.card_singleton` `le_refl`
`factors_eq_zero` 📖	mathematical	—	`factors` `Multiset` `Multiset.instZero` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `exists_mem_factors` `factors_of_isUnit`
`factors_mul` 📖	mathematical	—	`Multiset.Rel` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `factors` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Multiset` `Multiset.instAdd`	—	`factors_unique` `irreducible_of_factor` `Multiset.mem_add` `Associated.trans` `factors_prod` `mul_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `Multiset.prod_add` `Associated.symm` `Associated.mul_mul`
`factors_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`factors` `Multiset` `Multiset.instZero`	—	`factors_one` `factors_rel_of_associated` `associated_one_iff_isUnit`
`factors_one` 📖	mathematical	—	`factors` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instZero`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `exists_prime_factors` `Multiset.rel_zero_right` `factors_unique` `irreducible_of_factor` `Multiset.notMem_zero` `Multiset.prod_zero` `factors_prod` `one_ne_zero` `NeZero.one`
`factors_pos` 📖	mathematical	—	`Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `Multiset.instZero` `factors` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`bot_lt_iff_ne_bot` `not_iff_not` `factors_eq_zero`
`factors_pow` 📖	mathematical	—	`Multiset.Rel` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `factors` `Monoid.toNatPow` `Multiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid`	—	`zero_nsmul` `pow_zero` `factors_one` `Multiset.rel_zero_right` `factors.congr_simp` `zero_pow` `factors_zero` `nsmul_zero` `pow_succ'` `succ_nsmul'` `Multiset.Rel.trans` `Associated.instIsTrans` `factors_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `Multiset.Rel.add` `Multiset.rel_refl_of_refl_on` `Associated.refl`
`factors_pow_count_prod` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Finset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.toFinset` `factors` `Monoid.toNatPow` `Multiset.count`	—	`Multiset.prod_sum` `Finset.prod_congr` `Multiset.prod_nsmul` `Multiset.prod_singleton` `Multiset.toFinset_sum_count_nsmul_eq` `factors_prod`
`factors_rel_of_associated` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Multiset.Rel` `factors`	—	`iff_iff_and_or_not_and_not` `Associated.eq_zero_iff` `factors_zero` `factors_unique` `irreducible_of_factor` `Associated.trans` `factors_prod` `Associated.symm`
`factors_unique` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associated` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Multiset.Rel`	—	`prime_factors_unique` `toIsCancelMulZero` `irreducible_iff_prime`
`iff_exists_prime_factors` 📖	mathematical	—	`UniqueFactorizationMonoid` `Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	—	`exists_prime_factors` `of_exists_prime_factors`
`isRelPrime_iff_no_prime_factors` 📖	mathematical	—	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime`	—	`Prime.not_unit` `WfDvdMonoid.isRelPrime_of_no_irreducible_factors` `toIsWellFounded` `irreducible_iff_prime`
`of_existsUnique_irreducible_factors` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associated` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.Rel`	`UniqueFactorizationMonoid`	—	`of_exists_prime_factors` `irreducible_iff_prime_of_existsUnique_irreducible_factors`
`of_exists_prime_factors` 📖	mathematical	`Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`UniqueFactorizationMonoid`	—	`WfDvdMonoid.of_exists_prime_factors` `irreducible_iff_prime_of_exists_prime_factors`

WfDvdMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_wellFounded_associates` 📖	mathematical	—	`WfDvdMonoid` `WellFoundedLT` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLT` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid`	—	`wellFoundedLT_associates` `of_wellFoundedLT_associates`
`of_exists_prime_factors` 📖	mathematical	`Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`WfDvdMonoid`	—	`RelHomClass.wellFounded` `RelHom.instRelHomClass` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `MulZeroClass.mul_zero` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid` `Multiset.card_pos` `associated_one_iff_isUnit` `Multiset.prod_zero` `Associated.symm` `Multiset.card_add` `Multiset.card_eq_card_of_rel` `prime_factors_unique` `Multiset.mem_add` `Multiset.prod_add` `Associated.instIsTrans` `Associated.mul_mul` `wellFounded_lt`
`of_wellFoundedLT_associates` 📖	mathematical	—	`WfDvdMonoid`	—	`of_wfDvdMonoid_associates` `Associates.dvdNotUnit_iff_lt` `IsWellFounded.wf`
`of_wfDvdMonoid_associates` 📖	mathematical	—	`WfDvdMonoid`	—	`Function.Surjective.wellFounded_iff` `Associates.mk_surjective` `Associates.mk_dvdNotUnit_mk_iff` `wellFounded_dvdNotUnit`
`wellFoundedLT_associates` 📖	mathematical	—	`WellFoundedLT` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLT` `Associates.instPreorder` `CommMonoidWithZero.toCommMonoid`	—	`Associates.dvdNotUnit_of_lt` `wellFounded_dvdNotUnit` `wfDvdMonoid_associates`
`wfDvdMonoid_associates` 📖	mathematical	—	`WfDvdMonoid` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associates.instCommMonoidWithZero`	—	`Function.Surjective.wellFounded_iff` `Associates.mk_surjective` `Associates.mk_dvdNotUnit_mk_iff` `wellFounded_dvdNotUnit`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff_prime_of_existsUnique_irreducible_factors` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associated` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.Rel`	`Prime`	—	`Irreducible.ne_zero` `Irreducible.not_isUnit` `NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `MulZeroClass.mul_zero` `left_ne_zero_of_mul` `right_ne_zero_of_mul` `Multiset.mem_cons` `Multiset.mem_add` `Associated.instIsTrans` `Multiset.prod_cons` `Associated.mul_left` `Associated.mul_mul` `Associated.symm` `Multiset.prod_add` `Multiset.exists_mem_of_rel_of_mem` `Multiset.mem_cons_self` `Associated.dvd_iff_dvd_left` `Associated.dvd_iff_dvd_right` `Multiset.dvd_prod` `Prime.irreducible`
`irreducible_iff_prime_of_exists_prime_factors` 📖	mathematical	`Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Irreducible`	—	`prime_factors_irreducible` `Associated.prime_iff` `Multiset.mem_singleton_self` `Prime.irreducible`
`prime_factors_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Prime` `Associated` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Multiset` `Multiset.instSingleton`	—	`Multiset.induction_on` `Irreducible.not_isUnit` `associated_one_iff_isUnit` `Associated.symm` `Multiset.exists_mem_of_ne_zero` `Irreducible.isUnit_or_isUnit` `mul_right_comm` `mul_assoc` `Multiset.prod_cons` `Multiset.cons_erase` `mul_comm` `isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid` `Multiset.mem_cons_self` `mul_one`
`prime_factors_unique` 📖	mathematical	`Prime` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	`Multiset.Rel`	—	`Multiset.induction_on` `Multiset.rel_zero_left` `Multiset.eq_zero_of_forall_notMem` `Associated.symm` `Prime.not_unit` `isUnit_iff_dvd_one` `Dvd.dvd.trans` `Multiset.dvd_prod` `exists_associated_mem_of_dvd_prod` `Associated.dvd_iff_dvd_right` `Multiset.prod_cons` `Multiset.cons_erase` `Multiset.mem_of_mem_erase` `Associated.of_mul_left` `Prime.ne_zero`

---

← Back to Index