# 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`

.