Commit 2024-07-03 02:57 e5344068

View on Github →

chore(GroupTheory/MonoidLocalization): Change Localization to an abbrev of OreLocalization. (#13943)

Estimated changes

modified def Localization.mk
modified theorem Localization.mk_eq_mk_iff
modified theorem Localization.mk_one
modified theorem Localization.mk_pow
modified theorem Localization.mk_zero
deleted def Localization
modified theorem Localization.neg_mk
modified theorem OreLocalization.smul_oreDiv