Commit 2024-03-01 06:30 c7394bfb
View on Github →feat(RingTheory/UniqueFactorizationDomain): add WfDvdMonoid.max_power_factor[']
and multiplicity.finite_of_not_isUnit
(#11066)
- makes
UniqueFactorizationMonoid.max_power_factor
obsolete - makes the proof of
multiplicity.finite_prime_left
trivial - relax the condition of
exists_reduced_fraction'