Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 20:23 3e1d4d32

View on Github →

feat(algebra/gcd_monoid): associates lemmas (#10705)

Estimated changes

Modified src/algebra/gcd_monoid/basic.lean

added theorem associates.mk_out

added theorem associates.out_injective

modified theorem associates.out_mk

added def associates_equiv_of_unique_units

Modified src/ring_theory/int/basic.lean