Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.localization.r_eq_r'

Modification history

2020-06-04 15:38
src/group_theory/monoid_localization.lean
feat(ring/localization): add construction of localization as a quotient type (#2922)
Deleted submonoid.localization.r_eq_r'View on Github →
2020-03-06 19:21
src/group_theory/monoid_localization.lean
refactor(group_theory/monoid_localization): use characteristic predicate (#2004) …
Added submonoid.localization.r_eq_r'View on Github →