Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-15 19:32 871a36fc

View on Github →

feat(group_theory/monoid_localization) add localizations of commutative monoids at submonoids (#1798)

1st half of monoid_localization
change in implementation notes
fixing naming clashes
change additive version's name
oops, had a /- instead of /--
generalize comm_monoid instance
remove notes to self
responding to PR comments

Estimated changes

Modified src/group_theory/congruence.lean

modified def con.ker_lift

Created src/group_theory/monoid_localization.lean

added theorem add_submonoid.r'.add

added theorem add_submonoid.r'.transitive

added def add_submonoid.r'

added def monoid_localization.aux

added theorem monoid_localization.exists_rep

added theorem monoid_localization.funext

added theorem monoid_localization.ind

added theorem monoid_localization.induction_on

added theorem monoid_localization.is_unit_of_of_comp

added def monoid_localization.lift'

added theorem monoid_localization.lift'_apply_of

added theorem monoid_localization.lift'_comp_of

added theorem monoid_localization.lift'_eq_iff

added theorem monoid_localization.lift'_mk

added theorem monoid_localization.lift'_of

added theorem monoid_localization.lift_apply_of

added theorem monoid_localization.lift_comp_of

added theorem monoid_localization.lift_eq_iff

added theorem monoid_localization.lift_mk

added theorem monoid_localization.lift_of

added theorem monoid_localization.lift_on_beta

added def monoid_localization.map

added theorem monoid_localization.map_comp_map

added theorem monoid_localization.map_comp_of

added theorem monoid_localization.map_eq

added theorem monoid_localization.map_ext

added theorem monoid_localization.map_id

added theorem monoid_localization.map_map

added theorem monoid_localization.map_mk

added theorem monoid_localization.map_of

added def monoid_localization.mk

added theorem monoid_localization.mk_eq

added theorem monoid_localization.mk_eq_iff_of_eq

added theorem monoid_localization.mk_eq_mul_mk_one

added theorem monoid_localization.mk_eq_of_eq

added theorem monoid_localization.mk_is_unit'

added theorem monoid_localization.mk_is_unit

added theorem monoid_localization.mk_mul_cancel_left

added theorem monoid_localization.mk_mul_cancel_right

added theorem monoid_localization.mk_mul_mk

added theorem monoid_localization.mk_self'

added theorem monoid_localization.mk_self

added def monoid_localization.of

added theorem monoid_localization.of_eq_mk

added theorem monoid_localization.of_is_unit'

added theorem monoid_localization.of_is_unit

added theorem monoid_localization.of_ker_iff

added theorem monoid_localization.of_mul_mk

added theorem monoid_localization.one_rel

added theorem monoid_localization.r_le_ker_aux

added def monoid_localization.to_units

added theorem monoid_localization.to_units_inv

added theorem monoid_localization.to_units_map_inv

added theorem monoid_localization.to_units_mk

added def monoid_localization.units_restrict

added theorem monoid_localization.units_restrict_mul

added def monoid_localization

added def submonoid.r'

added def submonoid.r

added theorem submonoid.r_eq_r'