Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-16 09:19 f7a7c272

View on Github →

chore(ring_theory/ideal/local_ring): golf some proofs, add missing lemma (#14157)

Estimated changes

Modified src/algebra/group/units.lean

added theorem units.eq_iff_inv_mul

modified theorem units.inv_eq_of_mul_eq_one_right

Modified src/ring_theory/ideal/local_ring.lean