mathlib3

6d2a0512 - feat(algebra/covariant_and_contravariant): API for covariant_and_contravariant (#7889)

feat(algebra/covariant_and_contravariant): API for covariant_and_contravariant (#7889) This PR introduces more API for `covariant` and `contravariant` stuff . Besides the API, I have not actually made further use of the typeclasses or of the API. This happens in subsequent PRs. This is a step towards PR #7645.