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'

Estimated changes