Commit 2023-05-10 09:29 2de98a00

View on Github →

feat(RingTheory/UniqueFactorizationDomain) : add lemma max_power_factor as in #18830 (#3558) Add lemma max_powerFactor needed in leanprover-community/mathlib#18830 and modified there.

Estimated changes

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

modified theorem UniqueFactorizationMonoid.count_normalizedFactors_eq'

modified theorem UniqueFactorizationMonoid.count_normalizedFactors_eq

modified theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors

added theorem UniqueFactorizationMonoid.max_power_factor

modified theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors