Commit 2021-06-11 21:18 dd600354

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.