Commit 2023-04-24 11:35 877237e2

View on Github →

feat: Order on the localization (#3567) Match https://github.com/leanprover-community/mathlib/pull/18724 and https://github.com/leanprover-community/mathlib/pull/18846

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization.lean

added def Localization.mkOrderEmbedding

added theorem Localization.mk_eq_mk_iff'

added theorem Localization.mk_le_mk

added theorem Localization.mk_left_injective

added theorem Localization.mk_lt_mk

added def Localization.recOnSubsingleton₂