Commit 2023-01-30 10:29 41e9d745

View on Github →

feat: port GroupTheory.Monoid.Localization (#1777)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/MonoidLocalization.lean

added theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp

added theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq

added structure AddSubmonoid.LocalizationMap

added def Localization.Away.invSelf

added theorem Localization.Away.mk_eq_monoidOf_mk'

added def Localization.Away.monoidOf

added def Localization.Away

added theorem Localization.ind

added theorem Localization.induction_on

added theorem Localization.induction_on₂

added theorem Localization.induction_on₃

added def Localization.liftOn

added theorem Localization.liftOn_mk'

added theorem Localization.liftOn_mk

added theorem Localization.liftOn_zero

added def Localization.liftOn₂

added theorem Localization.liftOn₂_mk'

added theorem Localization.liftOn₂_mk

added def Localization.mk

added theorem Localization.mk_eq_mk_iff

added theorem Localization.mk_eq_monoidOf_mk'

added theorem Localization.mk_eq_monoidOf_mk'_apply

added theorem Localization.mk_mul

added theorem Localization.mk_one

added theorem Localization.mk_one_eq_monoidOf_mk

added theorem Localization.mk_pow

added theorem Localization.mk_self

added theorem Localization.mk_zero

added def Localization.monoidOf

added theorem Localization.mulEquivOfQuotient_apply

added theorem Localization.mulEquivOfQuotient_mk'

added theorem Localization.mulEquivOfQuotient_mk

added theorem Localization.mulEquivOfQuotient_monoidOf

added theorem Localization.mulEquivOfQuotient_symm_mk'

added theorem Localization.mulEquivOfQuotient_symm_mk

added theorem Localization.mulEquivOfQuotient_symm_monoidOf

added theorem Localization.ndrec_mk

added theorem Localization.one_rel

added def Localization.r'

added def Localization.r

added theorem Localization.r_eq_r'

added theorem Localization.r_iff_exists

added theorem Localization.r_of_eq

added def Localization.rec

added theorem Localization.smul_mk

added def Localization

added def MonoidHom.toLocalizationMap

added theorem Submonoid.LocalizationMap.AwayMap.lift_comp

added theorem Submonoid.LocalizationMap.AwayMap.lift_eq

added def Submonoid.LocalizationMap.AwayMap

added theorem Submonoid.LocalizationMap.comp_eq_of_eq

added theorem Submonoid.LocalizationMap.epic_of_localizationMap

added theorem Submonoid.LocalizationMap.eq_iff_eq

added theorem Submonoid.LocalizationMap.eq_iff_exists

added theorem Submonoid.LocalizationMap.eq_mk'_iff_mul_eq

added theorem Submonoid.LocalizationMap.eq_of_eq

added theorem Submonoid.LocalizationMap.exists_of_sec_mk'

added theorem Submonoid.LocalizationMap.ext

added theorem Submonoid.LocalizationMap.ext_iff

added theorem Submonoid.LocalizationMap.inv_inj

added theorem Submonoid.LocalizationMap.inv_unique

added theorem Submonoid.LocalizationMap.isUnit_comp

added theorem Submonoid.LocalizationMap.lift_comp

added theorem Submonoid.LocalizationMap.lift_eq

added theorem Submonoid.LocalizationMap.lift_eq_iff

added theorem Submonoid.LocalizationMap.lift_id

added theorem Submonoid.LocalizationMap.lift_injective_iff

added theorem Submonoid.LocalizationMap.lift_left_inverse

added theorem Submonoid.LocalizationMap.lift_mk'

added theorem Submonoid.LocalizationMap.lift_mk'_spec

added theorem Submonoid.LocalizationMap.lift_mul_left

added theorem Submonoid.LocalizationMap.lift_mul_right

added theorem Submonoid.LocalizationMap.lift_of_comp

added theorem Submonoid.LocalizationMap.lift_spec

added theorem Submonoid.LocalizationMap.lift_spec_mul

added theorem Submonoid.LocalizationMap.lift_surjective_iff

added theorem Submonoid.LocalizationMap.lift_unique

added theorem Submonoid.LocalizationMap.map_comp

added theorem Submonoid.LocalizationMap.map_comp_map

added theorem Submonoid.LocalizationMap.map_eq

added theorem Submonoid.LocalizationMap.map_id

added theorem Submonoid.LocalizationMap.map_left_cancel

added theorem Submonoid.LocalizationMap.map_map

added theorem Submonoid.LocalizationMap.map_mk'

added theorem Submonoid.LocalizationMap.map_mul_left

added theorem Submonoid.LocalizationMap.map_mul_right

added theorem Submonoid.LocalizationMap.map_right_cancel

added theorem Submonoid.LocalizationMap.map_spec

added theorem Submonoid.LocalizationMap.map_units

added theorem Submonoid.LocalizationMap.mk'_eq_iff_eq'

added theorem Submonoid.LocalizationMap.mk'_eq_iff_eq

added theorem Submonoid.LocalizationMap.mk'_eq_iff_eq_mul

added theorem Submonoid.LocalizationMap.mk'_eq_iff_mk'_eq

added theorem Submonoid.LocalizationMap.mk'_eq_of_eq'

added theorem Submonoid.LocalizationMap.mk'_eq_of_eq

added theorem Submonoid.LocalizationMap.mk'_mul

added theorem Submonoid.LocalizationMap.mk'_mul_cancel_left

added theorem Submonoid.LocalizationMap.mk'_mul_cancel_right

added theorem Submonoid.LocalizationMap.mk'_mul_eq_mk'_of_mul

added theorem Submonoid.LocalizationMap.mk'_one

added theorem Submonoid.LocalizationMap.mk'_sec

added theorem Submonoid.LocalizationMap.mk'_self'

added theorem Submonoid.LocalizationMap.mk'_self

added theorem Submonoid.LocalizationMap.mk'_spec'

added theorem Submonoid.LocalizationMap.mk'_spec

added theorem Submonoid.LocalizationMap.mk'_surjective

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_apply

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv_apply

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply

added theorem Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_eq_mulEquivOfLocalizations

added theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq

added theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map

added theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply

added theorem Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk'

added theorem Submonoid.LocalizationMap.mul_inv

added theorem Submonoid.LocalizationMap.mul_inv_left

added theorem Submonoid.LocalizationMap.mul_inv_right

added theorem Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul

added theorem Submonoid.LocalizationMap.mul_mk'_one_eq_mk'

added def Submonoid.LocalizationMap.ofMulEquivOfDom

added theorem Submonoid.LocalizationMap.ofMulEquivOfDom_apply

added theorem Submonoid.LocalizationMap.ofMulEquivOfDom_comp

added theorem Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm

added theorem Submonoid.LocalizationMap.ofMulEquivOfDom_eq

added theorem Submonoid.LocalizationMap.ofMulEquivOfDom_id

added def Submonoid.LocalizationMap.ofMulEquivOfLocalizations

added theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply

added theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_comp

added theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq

added theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq

added theorem Submonoid.LocalizationMap.ofMulEquivOfLocalizations_id

added theorem Submonoid.LocalizationMap.of_mulEquivOfMulEquiv

added theorem Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply

added theorem Submonoid.LocalizationMap.sec_spec'

added theorem Submonoid.LocalizationMap.sec_spec

added theorem Submonoid.LocalizationMap.sec_zero_fst

added theorem Submonoid.LocalizationMap.surj

added theorem Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply'

added theorem Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply

added theorem Submonoid.LocalizationMap.toMap_injective

added structure Submonoid.LocalizationMap

added def Submonoid.LocalizationWithZeroMap.toMonoidWithZeroHom

added structure Submonoid.LocalizationWithZeroMap