Commit 2021-06-11 21:18 dd600354
View on Github →chore(algebra/{covariant_and_contravariant + ordered_monoid_lemmas}): new file covariant_and_contravariant (#7890)
This PR creates a new file algebra/covariant_and_contravariant
and moves the part of algebra/ordered_monoid_lemmas
dealing exclusively with covariant
and contravariant
into it.
It also rearranges the documentation, with a view to the later PRs, building up to #7645.
The discrepancy between the added and removed lines is entirely due to longer documentation: no actual Lean code has changed, except, of course, for the import
in algebra/ordered_monoid_lemmas
that now uses covariant_and_contravariant
.