Commit 2023-11-18 10:10 8759327f

View on Github →

feat: some lemmas about UniqueFactorizationMonoids (#8486) From flt-regular.

Estimated changes

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

added theorem UniqueFactorizationMonoid.factors_pow_count_prod

added theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff

added theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod