Commit 2026-03-11 20:11 d2d3074a

View on Github →

feat(RingTheory/UniqueFactorizationDomain/Multiplicity): more API (#36381) This adds a few API lemmas on factorization in UniqueFactorizationMonoids. It also includes a minor cleanup of sections and variables. The results will be useful for proving the Northcott property for heights on number fields.

Estimated changes

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

added theorem UniqueFactorizationMonoid.associated_finprod_pow_count

modified theorem UniqueFactorizationMonoid.count_normalizedFactors_eq'

modified theorem UniqueFactorizationMonoid.count_normalizedFactors_eq

modified theorem UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors

added theorem UniqueFactorizationMonoid.finprod_pow_count_eq_of_subsingleton_units

added theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors