mathlib3

7e779677 - refactor(localization): shorten proofs (#796)

refactor(localization): shorten proofs (#796) * feat(algebra/group): units.coe_map * refactor(localization): shorten proofs * swap order of equality in ring_equiv.symm_to_equiv