mathlib3
2e9f708d - feat(algebra/ordered_monoid): order_embedding.mul_left (#9127)

Commit

5 years ago

feat(algebra/ordered_monoid): order_embedding.mul_left (#9127)

Author

kim-em

kim-em

Parents

Loading