Commit 2022-10-17 21:30 d0b0a734

View on Github →

feat: port Algebra/CovariantAndContravariant (#467) These are mostly instances required so that lemmas needed for linarith actually fire in the presence of LinearOrderedCommRing.

Estimated changes

added theorem Contravariant.flip
added def Contravariant
added theorem Covariant.flip
added def Covariant
added theorem act_rel_act_of_rel
added theorem covariant_flip_mul_iff
added theorem flip_mul
added theorem rel_iff_cov
added theorem rel_of_act_rel_act
added theorem Antitone.comp_monotone
added theorem Monotone.comp_antitone