Commit 2024-07-18 05:31 5589a75e

View on Github →

chore(UniqueFactorizationMonoid): make ufm_of_decomposition_of_wfDvdMonoid an instance (#14771)

Estimated changes

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

deleted theorem ufm_of_decomposition_of_wfDvdMonoid

added theorem ufm_of_gcd_of_wfDvdMonoid