FactorSet

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

Statistics

Metric	Count
Definitions `BfactorSetMem`, `FactorSet`, `prod`, `FactorSetMem`, `bcount`, `count`, `factors'`, `instLattice`, `instMax`, `instMembershipFactorSet`, `instMin`	11
Theorems `coe_add`, `prod_eq_zero_iff`, `sup_add_inf_eq_add`, `unique`, `coprime_iff_inf_one`, `count_eq_zero_of_ne`, `count_factors_eq_find_of_dvd_pow`, `count_le_count_of_factors_le`, `count_le_count_of_le`, `count_mul`, `count_mul_of_coprime`, `count_mul_of_coprime'`, `count_ne_zero_iff_dvd`, `count_of_coprime`, `count_pow`, `count_reducible`, `count_self`, `count_some`, `count_zero`, `dvd_count_of_dvd_count_mul`, `dvd_count_pow`, `dvd_of_mem_factors`, `dvd_of_mem_factors'`, `eq_factors_of_eq_counts`, `eq_of_eq_counts`, `eq_of_factors_eq_factors`, `eq_of_prod_eq_prod`, `eq_pow_count_factors_of_dvd_pow`, `eq_pow_find_of_dvd_irreducible_pow`, `eq_pow_of_mul_eq_pow`, `exists_prime_dvd_of_not_inf_one`, `factorSetMem_eq_mem`, `factors'_cong`, `factors_eq_some_iff_ne_zero`, `factors_eq_top_iff_zero`, `factors_le`, `factors_mk`, `factors_mono`, `factors_mul`, `factors_one`, `factors_prime_pow`, `factors_prod`, `factors_self`, `factors_subsingleton`, `factors_zero`, `irreducible_of_mem_factorSet`, `is_pow_of_dvd_count`, `le_of_count_ne_zero`, `map_subtype_coe_factors'`, `mem_factorSet_some`, `mem_factorSet_top`, `mem_factors'_iff_dvd`, `mem_factors'_of_dvd`, `mem_factors_iff_dvd`, `mem_factors_of_dvd`, `pow_factors`, `prime_pow_dvd_iff_le`, `prime_pow_le_iff_le_bcount`, `prod_add`, `prod_coe`, `prod_factors`, `prod_le`, `prod_mono`, `prod_top`, `reducible_notMem_factorSet`, `sup_mul_inf`	66
Total	77

Associates

Definitions

Name	Category	Theorems
`BfactorSetMem` 📖	MathDef	—
`FactorSet` 📖	CompOp	20 math math: `factors_mul`, `prod_top`, `pow_factors`, `factorSetMem_eq_mem`, `count_zero`, `factors_zero`, `factors_subsingleton`, `prod_add`, `factors_le`, `reducible_notMem_factorSet`, `factors_mono`, `mem_factorSet_top`, `mem_factors_iff_dvd`, `factors_eq_top_iff_zero`, `count_reducible`, `mem_factors_of_dvd`, `prod_le`, `factors_one`, `FactorSet.sup_add_inf_eq_add`, `FactorSet.prod_eq_zero_iff`
`FactorSetMem` 📖	MathDef	1 math math: `factorSetMem_eq_mem`
`bcount` 📖	CompOp	1 math math: `prime_pow_le_iff_le_bcount`
`count` 📖	CompOp	35 math math: `dvd_count_pow`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal`, `prime_pow_dvd_iff_le`, `finite_factors`, `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg`, `FractionalIdeal.count_well_defined`, `eq_pow_count_factors_of_dvd_pow`, `IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg`, `count_self`, `count_of_coprime`, `FractionalIdeal.finprod_heightOneSpectrum_factorization`, `count_some`, `count_zero`, `FractionalIdeal.count_ne_zero`, `count_le_count_of_le`, `count_pow`, `Ideal.finite_mulSupport_coe`, `count_mul_of_coprime'`, `count_factors_eq_find_of_dvd_pow`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `Ideal.count_associates_eq`, `count_mul`, `count_le_count_of_factors_le`, `Ideal.finprod_count`, `count_reducible`, `count_eq_zero_of_ne`, `Ideal.finprod_heightOneSpectrum_factorization_coe`, `FractionalIdeal.finite_factors'`, `count_associates_factors_eq`, `Ideal.count_associates_eq'`, `count_mul_of_coprime`, `FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction`, `Ideal.finprod_not_dvd`, `Ideal.finite_mulSupport_inv`, `FractionalIdeal.count_coe`
`factors'` 📖	CompOp	5 math math: `factors_mk`, `map_subtype_coe_factors'`, `mem_factors'_iff_dvd`, `factors'_cong`, `mem_factors'_of_dvd`
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `sup_mul_inf`
`instMembershipFactorSet` 📖	CompOp	6 math math: `factorSetMem_eq_mem`, `mem_factorSet_some`, `reducible_notMem_factorSet`, `mem_factorSet_top`, `mem_factors_iff_dvd`, `mem_factors_of_dvd`
`instMin` 📖	CompOp	2 math math: `sup_mul_inf`, `coprime_iff_inf_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_iff_inf_one` 📖	mathematical	—	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instMin` `instOne` `Prime`	—	`Prime.not_unit` `isUnit_of_dvd_one` `le_inf` `mk_le_mk_of_dvd` `Mathlib.Tactic.Contrapose.contrapose₁` `exists_prime_dvd_of_not_inf_one`
`count_eq_zero_of_ne` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `factors`	—	`not_ne_iff` `associated_iff_eq` `Unique.instSubsingleton` `Irreducible.associated_of_dvd` `le_of_count_ne_zero` `Irreducible.ne_zero`
`count_factors_eq_find_of_dvd_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow`	`Nat.find` `count` `factors`	—	`le_antisymm` `Nat.find_le` `mul_one` `eq_pow_count_factors_of_dvd_pow` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `UniqueFactorizationMonoid.toIsCancelMulZero` `Irreducible.ne_zero` `subsingleton_or_nontrivial` `Unique.instSubsingleton` `Quotient.instSubsingletonQuotient` `Nat.find.congr_simp` `count_pow` `count_self` `count_le_count_of_le` `Nat.find_spec`
`count_le_count_of_factors_le` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `FactorSet` `Preorder.toLE` `WithTop.instPreorder` `Multiset` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `factors`	`count`	—	`count.congr_simp` `factors.congr_simp` `factors_zero` `factors_eq_some_iff_ne_zero` `count_some` `Multiset.count_le_of_le` `WithTop.coe_le_coe`
`count_le_count_of_le` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid`	`count` `factors`	—	`count_le_count_of_factors_le` `factors_mono`
`count_mul` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `factors` `instMul` `CommMonoidWithZero.toCommMonoid`	—	`exists_non_zero_rep` `factors_mul` `FactorSet.coe_add` `count_some` `Multiset.count_add`
`count_mul_of_coprime` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Prime`	`count` `factors` `instMul` `CommMonoidWithZero.toCommMonoid`	—	`count.congr_simp` `factors.congr_simp` `factors_zero` `MulZeroClass.zero_mul` `count_of_coprime` `count_mul` `add_zero`
`count_mul_of_coprime'` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Prime`	`count` `factors` `instMul` `CommMonoidWithZero.toCommMonoid`	—	`count.congr_simp` `factors.congr_simp` `MulZeroClass.zero_mul` `factors_zero` `MulZeroClass.mul_zero` `count_mul` `count_of_coprime` `zero_add` `add_zero`
`count_ne_zero_iff_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`mk_le_mk_iff_dvd` `le_of_count_ne_zero` `mk_ne_zero` `LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `Nat.instZeroLEOneClass` `prime_pow_dvd_iff_le` `pow_one`
`count_of_coprime` 📖	mathematical	`Prime` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Irreducible`	`count` `factors`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `le_of_count_ne_zero` `UniqueFactorizationMonoid.irreducible_iff_prime` `ufm`
`count_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `factors` `Monoid.toNatPow`	—	`pow_zero` `factors_one` `MulZeroClass.zero_mul` `count_zero` `pow_succ'` `count_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `UniqueFactorizationMonoid.toIsCancelMulZero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt`
`count_reducible` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `Pi.instZero` `FactorSet` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	—
`count_self` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `factors`	—	`count.congr_simp` `factors_self` `count_some` `Multiset.count_eq_one_of_mem`
`count_some` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `WithTop.some` `Multiset` `Multiset.count`	—	—
`count_zero` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `FactorSet` `WithTop.zero` `Multiset` `Multiset.instZero`	—	—
`dvd_count_of_dvd_count_mul` 📖	—	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Prime` `count` `factors` `instMul` `CommMonoidWithZero.toCommMonoid`	—	—	`count.congr_simp` `factors.congr_simp` `factors_zero` `MulZeroClass.zero_mul` `count_of_coprime` `dvd_zero` `count_mul`
`dvd_count_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`count` `factors` `Monoid.toNatPow`	—	`count_pow` `dvd_mul_right`
`dvd_of_mem_factors` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `FactorSet` `instMembershipFactorSet` `factors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `instCommMonoidWithZero`	—	`eq_or_ne` `dvd_zero` `exists_non_zero_rep` `factors_prod` `prod_coe` `Multiset.dvd_prod` `Multiset.mem_map` `irreducible_of_mem_factorSet` `mem_factorSet_some`
`dvd_of_mem_factors'` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `Multiset` `Multiset.instMembership` `factors'`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`dvd_of_mem_factors` `mem_factorSet_some`
`eq_factors_of_eq_counts` 📖	—	`count` `factors`	—	—	`factors_eq_some_iff_ne_zero` `Multiset.ext'` `count.congr_simp` `count_some`
`eq_of_eq_counts` 📖	—	`count` `factors`	—	—	`eq_of_factors_eq_factors` `eq_factors_of_eq_counts`
`eq_of_factors_eq_factors` 📖	—	`factors`	—	—	`factors_prod`
`eq_of_prod_eq_prod` 📖	—	`FactorSet.prod`	—	—	`FactorSet.unique`
`eq_pow_count_factors_of_dvd_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow`	`count` `factors`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `count.congr_simp` `factors_subsingleton` `Quotient.instSubsingletonQuotient` `pow_ne_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `UniqueFactorizationMonoid.toIsCancelMulZero` `Irreducible.ne_zero` `ne_zero_of_dvd_ne_zero` `eq_of_eq_counts` `count_pow` `count_eq_zero_of_ne` `MulZeroClass.mul_zero` `count_le_count_of_le` `count_self` `mul_one`
`eq_pow_find_of_dvd_irreducible_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Monoid.toNatPow`	`Nat.find`	—	`count_factors_eq_find_of_dvd_pow` `eq_pow_count_factors_of_dvd_pow`
`eq_pow_of_mul_eq_pow` 📖	—	`Prime` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero` `instMul` `CommMonoidWithZero.toCommMonoid` `Monoid.toNatPow`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Quotient.instSubsingletonQuotient` `pow_zero` `mul_eq_one` `Unique.instSubsingleton` `is_pow_of_dvd_count` `dvd_count_of_dvd_count_mul` `dvd_count_pow` `mul_eq_zero` `instNoZeroDivisors` `UniqueFactorizationMonoid.toIsCancelMulZero` `zero_pow`
`exists_prime_dvd_of_not_inf_one` 📖	mathematical	—	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `Multiset.prod_zero` `Multiset.exists_mem_of_ne_zero` `WithTop.coe_eq_coe` `WithTop.coe_inf` `UniqueFactorizationMonoid.irreducible_iff_prime` `dvd_of_mem_factors'` `Multiset.mem_inter` `Multiset.inf_eq_inter`
`factorSetMem_eq_mem` 📖	mathematical	—	`FactorSetMem` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `FactorSet` `instMembershipFactorSet`	—	—
`factors'_cong` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`factors'`	—	`eq_or_ne` `associated_zero_iff_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `Associated.symm` `Multiset.map_eq_map` `Subtype.coe_injective` `map_subtype_coe_factors'` `rel_associated_iff_map_eq_map` `UniqueFactorizationMonoid.factors_unique` `UniqueFactorizationMonoid.irreducible_of_factor` `Associated.trans` `UniqueFactorizationMonoid.factors_prod`
`factors_eq_some_iff_ne_zero` 📖	mathematical	—	`factors` `WithTop.some` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero`	—	`Iff.not` `factors_eq_top_iff_zero`
`factors_eq_top_iff_zero` 📖	mathematical	—	`factors` `Top.top` `FactorSet` `WithTop.top` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `factors_subsingleton` `Quotient.instSubsingletonQuotient` `factors_prod` `FactorSet.prod_eq_zero_iff` `UniqueFactorizationMonoid.toIsCancelMulZero` `factors_zero`
`factors_le` 📖	mathematical	—	`FactorSet` `Preorder.toLE` `WithTop.instPreorder` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `factors` `instPreorder` `CommMonoidWithZero.toCommMonoid`	—	`prod_mono` `factors_prod` `factors_mono`
`factors_mk` 📖	mathematical	—	`factors` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `WithTop.some` `Multiset` `Associates` `Irreducible` `instCommMonoidWithZero` `factors'`	—	`mk_eq_zero`
`factors_mono` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid`	`FactorSet` `WithTop.instPreorder` `Multiset` `Irreducible` `instCommMonoidWithZero` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `factors`	—	`factors_mul` `le_add_of_nonneg_right` `WithTop.addLeftMono` `Multiset.instAddLeftMono` `bot_le`
`factors_mul` 📖	mathematical	—	`factors` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instMul` `CommMonoidWithZero.toCommMonoid` `FactorSet` `WithTop.add` `Multiset` `Irreducible` `instCommMonoidWithZero` `Multiset.instAdd`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `factors_subsingleton` `WithTop.add_top` `FactorSet.unique` `eq_of_factors_eq_factors` `prod_add` `factors_prod`
`factors_one` 📖	mathematical	—	`factors` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instOne` `FactorSet` `WithTop.zero` `Multiset` `Irreducible` `instCommMonoidWithZero` `Multiset.instZero`	—	`FactorSet.unique` `factors_prod` `Multiset.prod_zero`
`factors_prime_pow` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`factors` `Monoid.toNatPow` `WithTop.some` `Multiset` `Multiset.replicate`	—	`FactorSet.unique` `factors_prod` `FactorSet.prod.eq_def` `Multiset.map_replicate` `Multiset.prod_replicate`
`factors_prod` 📖	mathematical	—	`FactorSet.prod` `factors`	—	`mk_surjective` `eq_or_ne` `factors_zero` `map_subtype_coe_factors'`
`factors_self` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`factors` `WithTop.some` `Multiset` `Multiset.instSingleton`	—	`FactorSet.unique` `factors_prod` `FactorSet.prod.eq_def` `Multiset.prod_singleton`
`factors_subsingleton` 📖	mathematical	—	`factors` `Top.top` `FactorSet` `WithTop.top` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero`	—	`Quotient.instSubsingletonQuotient` `Lean.Meta.FastSubsingleton.elim` `factors_zero`
`factors_zero` 📖	mathematical	—	`factors` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Top.top` `FactorSet` `WithTop.top` `Multiset` `Irreducible` `instCommMonoidWithZero`	—	—
`irreducible_of_mem_factorSet` 📖	mathematical	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `FactorSet` `instMembershipFactorSet`	`Irreducible` `instCommMonoidWithZero`	—	`by_contra` `reducible_notMem_factorSet`
`is_pow_of_dvd_count` 📖	mathematical	`count` `factors`	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `instCommMonoidWithZero`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Quotient.instSubsingletonQuotient` `exists_non_zero_rep` `Subtype.coe_eta` `count_some` `Multiset.exists_smul_of_dvd_count` `eq_of_factors_eq_factors` `pow_factors` `prod_factors` `WithBot.coe_nsmul`
`le_of_count_ne_zero` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid`	—	`pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `pow_one` `prime_pow_dvd_iff_le`
`map_subtype_coe_factors'` 📖	mathematical	—	`Multiset.map` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `factors'` `UniqueFactorizationMonoid.factors`	—	`UniqueFactorizationMonoid.irreducible_of_factor` `Multiset.map_pmap` `Multiset.pmap_eq_map`
`mem_factorSet_some` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`WithTop` `Multiset` `instMembershipFactorSet` `WithTop.some` `Multiset.instMembership`	—	—
`mem_factorSet_top` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`FactorSet` `instMembershipFactorSet` `Top.top` `WithTop.top` `Multiset`	—	—
`mem_factors'_iff_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Associates` `instCommMonoidWithZero` `Multiset` `Multiset.instMembership` `factors'` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`dvd_of_mem_factors'` `mem_factors'_of_dvd`
`mem_factors'_of_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`Associates` `instCommMonoidWithZero` `Multiset` `Multiset.instMembership` `factors'`	—	`UniqueFactorizationMonoid.exists_mem_factors_of_dvd` `UniqueFactorizationMonoid.irreducible_of_factor` `Multiset.mem_pmap` `mk_eq_mk_iff_associated`
`mem_factors_iff_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Associates` `FactorSet` `instMembershipFactorSet` `factors` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`dvd_of_mem_factors` `mem_factors_of_dvd`
`mem_factors_of_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`Associates` `FactorSet` `instMembershipFactorSet` `factors`	—	`mem_factorSet_some` `mem_factors'_of_dvd`
`pow_factors` 📖	mathematical	—	`factors` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `instCommMonoidWithZero` `FactorSet` `AddMonoid.toNatSMul` `WithTop.addMonoid` `Multiset` `Irreducible` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid`	—	`zero_nsmul` `pow_zero` `factors_one` `pow_succ` `succ_nsmul` `factors_mul`
`prime_pow_dvd_iff_le` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid` `Monoid.toNatPow` `count` `factors`	—	`count.eq_1` `prime_pow_le_iff_le_bcount`
`prime_pow_le_iff_le_bcount` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid` `Monoid.toNatPow` `bcount` `factors`	—	`exists_non_zero_rep` `nontrivial_of_ne` `bcount.eq_def` `Multiset.le_count_iff_replicate_le` `factors_le` `factors_prime_pow` `WithTop.coe_le_coe`
`prod_add` 📖	mathematical	—	`FactorSet.prod` `FactorSet` `WithTop.add` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `Multiset.instAdd` `instMul` `CommMonoidWithZero.toCommMonoid`	—	`MulZeroClass.zero_mul` `WithTop.add_top` `MulZeroClass.mul_zero` `FactorSet.coe_add` `prod_coe` `Multiset.map_add` `Multiset.prod_add`
`prod_coe` 📖	mathematical	—	`FactorSet.prod` `WithTop.some` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `Multiset.prod` `instCommMonoid` `CommMonoidWithZero.toCommMonoid` `Multiset.map`	—	—
`prod_factors` 📖	mathematical	—	`factors` `FactorSet.prod`	—	`FactorSet.unique` `factors_prod`
`prod_le` 📖	mathematical	—	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Preorder.toLE` `instPreorder` `CommMonoidWithZero.toCommMonoid` `FactorSet.prod` `FactorSet` `WithTop.instPreorder` `Multiset` `Irreducible` `instCommMonoidWithZero` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	—	`factors_mono` `prod_factors` `prod_mono`
`prod_mono` 📖	mathematical	`FactorSet` `Preorder.toLE` `WithTop.instPreorder` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `PartialOrder.toPreorder` `Multiset.instPartialOrder`	`instPreorder` `CommMonoidWithZero.toCommMonoid` `FactorSet.prod`	—	`top_unique` `prod_top` `le_refl` `prod_le_prod` `Multiset.map_le_map` `WithTop.coe_le_coe`
`prod_top` 📖	mathematical	—	`FactorSet.prod` `Top.top` `FactorSet` `WithTop.top` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `instCommMonoidWithZero` `instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—
`reducible_notMem_factorSet` 📖	mathematical	`Irreducible` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	`FactorSet` `instMembershipFactorSet`	—	`FactorSetMem.eq_1` `factorSetMem_eq_mem`
`sup_mul_inf` 📖	mathematical	—	`Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instMul` `CommMonoidWithZero.toCommMonoid` `instMax` `instMin`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `factors_subsingleton` `sup_of_le_left` `inf_of_le_left` `MulZeroClass.mul_zero` `instNoZeroDivisors` `Subsingleton.to_isCancelMulZero` `Quotient.instSubsingletonQuotient` `eq_of_factors_eq_factors` `prod_add` `prod_factors` `factors_mul` `FactorSet.sup_add_inf_eq_add`

Associates.FactorSet

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	8 math math: `Associates.prod_top`, `Associates.prod_add`, `Associates.prod_factors`, `Associates.prod_mono`, `Associates.factors_prod`, `Associates.prod_le`, `Associates.prod_coe`, `prod_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_add` 📖	mathematical	—	`WithTop.some` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates.instCommMonoidWithZero` `Multiset.instAdd` `WithTop` `WithTop.add`	—	—
`prod_eq_zero_iff` 📖	mathematical	—	`prod` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Associates.instZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Top.top` `Associates.FactorSet` `WithTop.top` `Multiset` `Irreducible` `Associates.instCommMonoidWithZero`	—	`Associates.prod_coe` `Multiset.prod_eq_zero_iff` `Associates.instNoZeroDivisors` `Associates.instNontrivial` `Multiset.mem_map` `WithTop.coe_ne_top` `Irreducible.ne_zero` `Subtype.prop`
`sup_add_inf_eq_add` 📖	mathematical	—	`Associates.FactorSet` `WithTop.add` `Multiset` `Associates` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Irreducible` `Associates.instCommMonoidWithZero` `Multiset.instAdd` `SemilatticeSup.toMax` `WithTop.semilatticeSup` `Lattice.toSemilatticeSup` `Multiset.instLattice` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf`	—	`sup_of_le_left` `inf_of_le_right` `sup_of_le_right` `inf_of_le_left` `WithTop.add_top` `WithTop.coe_sup` `WithTop.coe_inf` `WithTop.coe_add` `WithTop.coe_eq_coe` `Multiset.union_add_inter`
`unique` 📖	—	`prod`	—	—	`prod_eq_zero_iff` `UniqueFactorizationMonoid.toIsCancelMulZero` `Associates.prod_top` `Multiset.map_eq_map` `Subtype.coe_injective` `Associates.unique'` `Multiset.mem_map`

---

← Back to Index