Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-07 23:35 7e779677

View on Github →

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

Estimated changes

Modified src/data/equiv/algebra.lean

added theorem ring_equiv.to_equiv_symm

added theorem ring_equiv.to_equiv_symm_apply

Modified src/ring_theory/localization.lean

modified theorem localization.lift'_apply_coe

added theorem localization.lift'_mk

added theorem localization.map_comp_map

added theorem localization.map_id

added theorem localization.map_map