Commit 2022-12-06 13:59 d3f6db58

View on Github →

feat: port Algebra.Order.Monoid.Basic (#872) mathlib3 SHA: 9b2660e1b25419042c8da10bf411aa3c67f14383

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Monoid/Basic.lean

added def Function.Injective.linearOrderedCommMonoid

added def Function.Injective.orderedCommMonoid

added def OrderEmbedding.mulLeft

added def OrderEmbedding.mulRight