Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-09 14:39 06c54b33

View on Github →

chore(ring_theory): introduce r_of_eq for localization

Estimated changes

Modified ring_theory/localization.lean

modified def localization.of_comm_ring

added theorem localization.r_of_eq

modified theorem localization.refl