Commit 2021-06-24 08:13 2f27046f

View on Github →

refactor(algebra/ordered_monoid): use covariant + contravariant typeclasses in algebra/ordered_monoid (#7999) Another stepping stone toward #7645.

Estimated changes

Modified src/algebra/covariant_and_contravariant.lean

Modified src/algebra/ordered_monoid.lean

modified theorem one_le