Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-22 09:26 831c4940

View on Github →

refactor(group_theory/monoid_localization): flip the direction of multiplication (#15584) In a future PR, this will allow localization and module_localization to be defeq. Mathematically this makes no difference. For now, only the primed localization.r' is defeq to localized_module.r.

Estimated changes

modified theorem localized_module.mk_eq
modified def localized_module.r
modified theorem localization.r_iff_exists
modified theorem localization.r_of_eq