Commit 2024-08-27 14:29 a0f40a65

View on Github →

feat: create aliases and lemmas for CovariantClass α α (· * ·) (· ≤ ·) etc (#13467) The first step towards removing CovariantClass and ContravariantClass.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean

added theorem Group.mulLeftReflectLE_of_mulLeftMono

added theorem Group.mulLeftReflectLT_of_mulLeftStrictMono

added theorem Group.mulRightReflectLE_of_mulRightMono

added theorem Group.mulRightReflectLT_of_mulRightStrictMono

added theorem mulLeftMono_of_mulLeftStrictMono

added theorem mulLeftReflectLT_of_mulLeftMono

added theorem mulLeftStrictMono_of_mulLeftReflectLE

added theorem mulRightMono_of_mulLeftMono

added theorem mulRightMono_of_mulRightStrictMono

added theorem mulRightReflectLE_of_mulLeftReflectLE

added theorem mulRightReflectLT_of_mulLeftReflectLT

added theorem mulRightReflectLT_of_mulRightMono

added theorem mulRightStrictMono_of_mulLeftStrictMono

added theorem mulRightStrictMono_of_mulRightReflectLE