NormalizedFactors

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

Statistics

Metric	Count
Definitions `normalizationMonoid`, `normalizedFactors`, `normalizedFactorsEquiv`	3
Theorems `normalizedFactors_eq`, `normalizedFactors_pow`, `associated_iff_normalizedFactors_eq_normalizedFactors`, `disjoint_normalizedFactors`, `dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors`, `dvd_iff_normalizedFactors_le_normalizedFactors`, `dvd_of_mem_normalizedFactors`, `dvd_of_normalized_factor`, `exists_associated_prime_pow_of_unique_normalized_factor`, `exists_mem_normalizedFactors`, `exists_mem_normalizedFactors_of_dvd`, `factors_eq_normalizedFactors`, `irreducible_of_normalized_factor`, `mem_normalizedFactors_eq_of_associated`, `mem_normalizedFactors_iff`, `mem_normalizedFactors_iff'`, `ne_zero_of_mem_normalizedFactors`, `normalize_normalized_factor`, `normalizedFactorsEquiv_apply`, `normalizedFactorsEquiv_symm_apply`, `normalizedFactors_eq_of_dvd`, `normalizedFactors_eq_zero_iff`, `normalizedFactors_irreducible`, `normalizedFactors_mul`, `normalizedFactors_multiset_prod`, `normalizedFactors_of_irreducible_pow`, `normalizedFactors_of_isUnit`, `normalizedFactors_one`, `normalizedFactors_pos`, `normalizedFactors_pow`, `normalizedFactors_prod_eq`, `normalizedFactors_prod_of_prime`, `normalizedFactors_zero`, `prime_of_normalized_factor`, `prod_normalizedFactors`, `prod_normalizedFactors_eq`, `zero_notMem_normalizedFactors`	37
Total	40

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalizedFactors_eq` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`UniqueFactorizationMonoid.normalizedFactors`	—	`UniqueFactorizationMonoid.toIsCancelMulZero` `Multiset.map_map` `Associates.rel_associated_iff_map_eq_map` `UniqueFactorizationMonoid.factors_rel_of_associated`

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalizedFactors_pow` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`UniqueFactorizationMonoid.normalizedFactors` `Monoid.toNatPow` `Multiset.replicate` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize`	—	`UniqueFactorizationMonoid.normalizedFactors_pow` `UniqueFactorizationMonoid.normalizedFactors_irreducible` `Multiset.nsmul_singleton`

UniqueFactorizationMonoid

Definitions

Name	Category	Theorems
`normalizationMonoid` 📖	CompOp	—
`normalizedFactors` 📖	CompOp	63 math math: `factors_eq_normalizedFactors`, `mem_normalizedFactors_iff`, `disjoint_normalizedFactors`, `Nat.factors_multiset_prod_of_irreducible`, `prod_normalizedFactors_eq_self`, `Ideal.count_normalizedFactors_eq`, `normalizedFactors_zero`, `Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count`, `Polynomial.leadingCoeff_mul_prod_normalizedFactors`, `normalizedFactorsEquivOfQuotEquiv_symm`, `normalizedFactors_mul`, `normalizedFactors_one`, `normalizedFactors_pos`, `normalizedFactors_prod_of_prime`, `PowerSeries.normalized_count_X_eq_of_coe`, `count_normalizedFactors_eq`, `normalizedFactors_nodup`, `exists_mem_normalizedFactors`, `normalizedFactors_of_isUnit`, `IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime`, `associated_iff_normalizedFactors_eq_normalizedFactors`, `count_span_normalizedFactors_eq_of_normUnit`, `irreducible_pow_sup`, `Nat.factors_eq`, `Nat.sum_divisors_filter_squarefree`, `exists_mem_normalizedFactors_of_dvd`, `mem_primeFactors`, `Ideal.mem_normalizedFactors_iff`, `count_le_of_ideal_ge`, `Irreducible.normalizedFactors_pow`, `normalizedFactors_irreducible`, `prod_normalizedFactors`, `Ideal.mem_primesOver_iff_mem_normalizedFactors`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity`, `normalizedFactors_prod_eq`, `emultiplicity_eq_count_normalizedFactors`, `count_span_normalizedFactors_eq`, `Polynomial.mem_normalizedFactors_iff`, `le_emultiplicity_iff_replicate_le_normalizedFactors`, `factorization_eq_count`, `normalizedFactors_pow`, `primeFactors_val_eq_normalizedFactors`, `IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count`, `mem_normalizedFactors_iff'`, `dvd_iff_normalizedFactors_le_normalizedFactors`, `Ideal.eq_prime_pow_mul_coprime`, `normalizedFactors_eq_zero_iff`, `KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map`, `count_normalizedFactors_eq'`, `normalizedFactors_of_irreducible_pow`, `count_associates_factors_eq`, `squarefree_iff_nodup_normalizedFactors`, `prod_normalizedFactors_eq`, `sup_eq_prod_inf_factors`, `Nat.divisors_filter_squarefree`, `zero_notMem_normalizedFactors`, `radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors`, `support_factorization`, `Associated.normalizedFactors_eq`, `Polynomial.normalizedFactors_cyclotomic_card`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `normalizedFactors_multiset_prod`, `dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors`
`normalizedFactorsEquiv` 📖	CompOp	2 math math: `normalizedFactorsEquiv_symm_apply`, `normalizedFactorsEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_iff_normalizedFactors_eq_normalizedFactors` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `normalizedFactors`	—	`Associated.normalizedFactors_eq` `Associated.trans` `Associated.symm` `prod_normalizedFactors` `trans` `Associated.instIsTrans` `Associated.refl`
`disjoint_normalizedFactors` 📖	mathematical	`IsRelPrime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `normalizedFactors`	—	`Multiset.disjoint_left` `dvd_of_mem_normalizedFactors` `Prime.not_unit` `prime_of_normalized_factor`
`dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors` 📖	mathematical	—	`DvdNotUnit` `Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `normalizedFactors`	—	`normalizedFactors_mul` `right_ne_zero_of_mul` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Multiset.instAddLeftMono` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `Multiset.instIsOrderedCancelAddMonoid` `dvdNotUnit_of_dvd_of_not_dvd` `dvd_iff_normalizedFactors_le_normalizedFactors` `LT.lt.le` `LT.lt.not_ge`
`dvd_iff_normalizedFactors_le_normalizedFactors` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `normalizedFactors`	—	`normalizedFactors_mul` `right_ne_zero_of_mul` `Multiset.instAddLeftMono` `Multiset.instAddLeftReflectLE` `Multiset.instCanonicallyOrderedAdd` `Associated.dvd_iff_dvd_left` `prod_normalizedFactors` `Associated.dvd_iff_dvd_right` `Multiset.prod_dvd_prod_of_le`
`dvd_of_mem_normalizedFactors` 📖	mathematical	`Multiset` `Multiset.instMembership` `normalizedFactors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`dvd_zero` `dvd_trans` `Multiset.dvd_prod` `Associated.dvd` `prod_normalizedFactors`
`dvd_of_normalized_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `normalizedFactors`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`dvd_of_mem_normalizedFactors`
`exists_associated_prime_pow_of_unique_normalized_factor` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow`	—	`prod_normalizedFactors` `Multiset.prod_replicate` `Multiset.eq_replicate_of_mem`
`exists_mem_normalizedFactors` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Multiset` `Multiset.instMembership` `normalizedFactors`	—	`WfDvdMonoid.exists_irreducible_factor` `toIsWellFounded` `exists_mem_normalizedFactors_of_dvd`
`exists_mem_normalizedFactors_of_dvd` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	`Multiset` `Multiset.instMembership` `normalizedFactors` `Associated`	—	`MulZeroClass.mul_zero` `factors_unique` `Multiset.mem_cons` `irreducible_of_normalized_factor` `Associated.symm` `Associated.instIsTrans` `prod_normalizedFactors` `Multiset.prod_cons` `Associated.mul_left` `Multiset.exists_mem_of_rel_of_mem`
`factors_eq_normalizedFactors` 📖	mathematical	—	`factors` `normalizedFactors` `NormalizationMonoid.ofUniqueUnits`	—	`Multiset.map_congr` `normalize_eq` `Multiset.map_id`
`irreducible_of_normalized_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `normalizedFactors`	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.irreducible` `toIsCancelMulZero` `prime_of_normalized_factor`
`mem_normalizedFactors_eq_of_associated` 📖	—	`Multiset` `Multiset.instMembership` `normalizedFactors` `Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	—	`normalize_normalized_factor` `normalize_eq_normalize_iff` `toIsCancelMulZero` `Associated.dvd_dvd`
`mem_normalizedFactors_iff` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `normalizedFactors` `Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	`prime_of_normalized_factor` `dvd_of_mem_normalizedFactors` `exists_mem_normalizedFactors_of_dvd` `Prime.irreducible` `toIsCancelMulZero` `associated_iff_eq`
`mem_normalizedFactors_iff'` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `normalizedFactors` `Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero`	—	`irreducible_of_normalized_factor` `normalize_normalized_factor` `dvd_of_mem_normalizedFactors` `exists_mem_factors_of_dvd` `Multiset.mem_map` `normalize_eq_normalize_iff_associated` `toIsCancelMulZero` `Associated.comm`
`ne_zero_of_mem_normalizedFactors` 📖	—	`Multiset` `Multiset.instMembership` `normalizedFactors`	—	—	`zero_notMem_normalizedFactors`
`normalize_normalized_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `normalizedFactors`	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize`	—	`normalizedFactors.eq_1` `exists_prime_factors` `factors.eq_1` `Multiset.map_congr` `instIsEmptyFalse` `Multiset.mem_map` `normalize_idem`
`normalizedFactorsEquiv_apply` 📖	mathematical	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `EquivLike.toFunLike` `Multiset` `Multiset.instMembership` `normalizedFactors`	`Equiv` `Equiv.instEquivLike` `normalizedFactorsEquiv`	—	—
`normalizedFactorsEquiv_symm_apply` 📖	mathematical	`DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize` `EquivLike.toFunLike` `Multiset` `Multiset.instMembership` `normalizedFactors`	`Equiv` `Equiv.instEquivLike` `Equiv.symm` `normalizedFactorsEquiv` `MulEquiv` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MulEquiv.instEquivLike` `MulEquiv.symm` `MulEquivClass.toMulEquiv`	—	—
`normalizedFactors_eq_of_dvd` 📖	—	`Multiset` `Multiset.instMembership` `normalizedFactors` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero`	—	—	`normalize_normalized_factor` `normalize_eq_normalize` `toIsCancelMulZero` `Irreducible.dvd_symm` `Prime.irreducible` `prime_of_normalized_factor`
`normalizedFactors_eq_zero_iff` 📖	mathematical	—	`normalizedFactors` `Multiset` `Multiset.instZero` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`not_iff_not` `normalizedFactors_pos` `pos_iff_ne_zero` `Multiset.instCanonicallyOrderedAdd`
`normalizedFactors_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`normalizedFactors` `Multiset` `Multiset.instSingleton` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize`	—	`prime_factors_irreducible` `prime_of_normalized_factor` `prod_normalizedFactors` `Irreducible.ne_zero` `Multiset.mem_singleton_self` `normalize_normalized_factor` `normalize_eq_normalize_iff` `toIsCancelMulZero` `dvd_dvd_iff_associated` `IsCancelMulZero.toIsLeftCancelMulZero`
`normalizedFactors_mul` 📖	mathematical	—	`normalizedFactors` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instAdd`	—	`toIsCancelMulZero` `Multiset.map_id'` `Multiset.map_congr` `normalize_normalized_factor` `Multiset.map_add` `Multiset.map_map` `Multiset.map_mk_eq_map_mk_of_rel` `factors_unique` `Multiset.mem_add` `irreducible_of_normalized_factor` `Multiset.prod_add` `Associated.trans` `Associated.mul_mul` `prod_normalizedFactors` `Associated.symm` `mul_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero`
`normalizedFactors_multiset_prod` 📖	mathematical	`Multiset` `Multiset.instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	`normalizedFactors` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.sum` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `Multiset.map`	—	`subsingleton_or_nontrivial` `normalizedFactors_one` `Multiset.eq_zero_of_forall_notMem` `Lean.Meta.FastSubsingleton.elim` `Multiset.induction` `Multiset.prod_cons` `Multiset.map_cons` `Multiset.sum_cons` `normalizedFactors_mul` `Multiset.mem_cons_self` `Multiset.prod_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `Multiset.mem_cons_of_mem`
`normalizedFactors_of_irreducible_pow` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`normalizedFactors` `Monoid.toNatPow` `Multiset.replicate` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize`	—	`normalizedFactors_pow` `normalizedFactors_irreducible` `Multiset.nsmul_singleton`
`normalizedFactors_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`normalizedFactors` `Multiset` `Multiset.instZero`	—	`eq_or_ne` `normalizedFactors_zero` `normalizedFactors_eq_zero_iff`
`normalizedFactors_one` 📖	mathematical	—	`normalizedFactors` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instZero`	—	`subsingleton_or_nontrivial` `exists_prime_factors` `Multiset.map_congr` `Multiset.rel_zero_right` `factors_unique` `irreducible_of_normalized_factor` `Multiset.notMem_zero` `prod_normalizedFactors` `one_ne_zero` `NeZero.one`
`normalizedFactors_pos` 📖	mathematical	—	`Multiset` `Preorder.toLT` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `Multiset.instZero` `normalizedFactors` `IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Multiset.exists_mem_of_ne_zero` `LT.lt.ne'` `Prime.not_unit` `prime_of_normalized_factor` `isUnit_of_dvd_unit` `dvd_of_mem_normalizedFactors` `exists_mem_normalizedFactors` `bot_lt_iff_ne_bot` `Multiset.eq_zero_iff_forall_notMem`
`normalizedFactors_pow` 📖	mathematical	—	`normalizedFactors` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid`	—	`normalizedFactors.congr_simp` `pow_zero` `normalizedFactors_one` `zero_nsmul` `zero_pow` `normalizedFactors_zero` `nsmul_zero` `pow_succ'` `succ_nsmul'` `normalizedFactors_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero`
`normalizedFactors_prod_eq` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`normalizedFactors` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `Multiset.map` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `MonoidWithZeroHom.funLike` `normalize`	—	`Multiset.induction` `Multiset.prod_zero` `normalizedFactors_one` `Multiset.map_zero` `Multiset.mem_cons_self` `Multiset.mem_cons_of_mem` `Multiset.empty_or_exists_mem` `Multiset.cons_zero` `Multiset.prod_singleton` `Multiset.map_singleton` `normalizedFactors_irreducible` `Multiset.prod_cons` `Multiset.map_cons` `normalizedFactors_mul` `Irreducible.ne_zero` `Multiset.prod_ne_zero` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero` `toIsCancelMulZero` `nontrivial_of_ne` `Multiset.singleton_add`
`normalizedFactors_prod_of_prime` 📖	mathematical	`Prime`	`normalizedFactors` `Multiset.prod` `CommMonoidWithZero.toCommMonoid`	—	`subsingleton_or_nontrivial` `normalizedFactors_one` `Multiset.eq_zero_of_forall_notMem` `prime_factors_unique` `toIsCancelMulZero` `prime_of_normalized_factor` `prod_normalizedFactors` `Multiset.prod_ne_zero_of_prime` `IsRightCancelMulZero.to_noZeroDivisors` `IsCancelMulZero.toIsRightCancelMulZero`
`normalizedFactors_zero` 📖	mathematical	—	`normalizedFactors` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `Multiset` `Multiset.instZero`	—	`Multiset.map_congr` `exists_prime_factors`
`prime_of_normalized_factor` 📖	mathematical	`Multiset` `Multiset.instMembership` `normalizedFactors`	`Prime`	—	`normalizedFactors.eq_1` `exists_prime_factors` `factors.eq_1` `Multiset.map_congr` `instIsEmptyFalse` `Multiset.mem_map` `Associated.prime_iff` `normalize_associated`
`prod_normalizedFactors` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Multiset.prod` `CommMonoidWithZero.toCommMonoid` `normalizedFactors`	—	`normalizedFactors.eq_1` `exists_prime_factors` `factors.eq_1` `Associated.trans` `Associates.mk_eq_mk_iff_associated` `Multiset.map_map` `Associates.mk_normalize`
`prod_normalizedFactors_eq` 📖	mathematical	—	`Multiset.prod` `CommMonoidWithZero.toCommMonoid` `normalizedFactors` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `MonoidWithZeroHom.funLike` `normalize`	—	`normalizedFactors.eq_1` `map_multiset_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `normalize_idem` `normalize_eq_normalize_iff` `toIsCancelMulZero` `dvd_dvd_iff_associated` `IsCancelMulZero.toIsLeftCancelMulZero` `prod_normalizedFactors`
`zero_notMem_normalizedFactors` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `normalizedFactors` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`Prime.ne_zero` `prime_of_normalized_factor`

---

← Back to Index