Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-22 06:16 2ae199f1

View on Github →

refactor(ring_theory/unique_factorization_domain): completes the refactor of unique_factorization_domain (#4156) Refactors unique_factorization_domain to unique_factorization_monoid unique_factorization_monoid is a predicate unique_factorization_monoid now requires no additive/subtractive structure

Estimated changes

deleted def associates.factors'
deleted def associates.factors
modified theorem associates.factors_mk
modified def associates.{u}
deleted theorem coprime_iff_gcd_eq_one
added theorem prime_factors_unique