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

added theorem add_submonoid.r'.add
added def add_submonoid.r'
added def submonoid.r'
added def submonoid.r
added theorem submonoid.r_eq_r'