Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-13 11:45 6d2a0512

View on Github →

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.

Estimated changes

Modified src/algebra/covariant_and_contravariant.lean

added theorem act_rel_act_of_rel

added theorem act_rel_act_of_rel_of_rel

added theorem act_rel_of_act_rel_of_rel_act_rel

added theorem act_rel_of_rel_of_act_rel

modified def contravariant

added theorem contravariant_flip_mul_iff

added theorem contravariant_lt_of_contravariant_le

added theorem covariant_flip_mul_iff

added theorem covariant_le_iff_contravariant_lt

added theorem covariant_le_of_covariant_lt

added theorem covariant_lt_iff_contravariant_le

added theorem covconv

added theorem group.covariant_iff_contravariant

added theorem rel_act_of_act_rel_act_of_rel_act

added theorem rel_act_of_rel_of_rel_act

added theorem rel_iff_cov

added theorem rel_of_act_rel_act

Modified src/algebra/ordered_group.lean

Modified src/algebra/ordered_monoid.lean

Modified src/algebra/ordered_monoid_lemmas.lean