Commit 2023-12-27 09:02 e0ae51d2

View on Github →

chore: Rename monotonicity of • lemmas in modules (#9302) Fix the names of the lemmas moved in #9241 to match the naming convention.

Estimated changes

Modified Mathlib/Algebra/Order/Module/Defs.lean

deleted def OrderIso.smulLeftDual

added def OrderIso.smulRightDual

modified theorem antitone_smul_left

deleted theorem smul_le_smul_iff_of_neg

added theorem smul_le_smul_iff_of_neg_left

deleted theorem smul_le_smul_of_nonpos

added theorem smul_le_smul_of_nonpos_left

deleted theorem smul_lt_smul_iff_of_neg

added theorem smul_lt_smul_iff_of_neg_left

deleted theorem smul_lt_smul_of_neg

added theorem smul_lt_smul_of_neg_left

deleted theorem smul_neg_iff_of_neg

added theorem smul_neg_iff_of_neg_left

deleted theorem smul_pos_iff_of_neg

added theorem smul_pos_iff_of_neg_left

added theorem strictAnti_smul_left

deleted theorem strict_anti_smul_left

Modified Mathlib/Algebra/Order/Module/Pointwise.lean

Modified Mathlib/Data/Real/Pointwise.lean