Commit 2023-12-26 22:33 299792d9

View on Github →

chore: Generalise monotonicity of • lemmas in modules (#9241) Sort the lemmas in Algebra.Order.Module into Algebra.Order.Module.Defs and Algebra.Order.Module.Pointwise. Generalise them. A later PR will rename the lemmas to better match the naming convention.

Estimated changes

deleted theorem BddAbove.smul_of_nonpos
deleted theorem BddBelow.smul_of_nonpos
deleted theorem antitone_smul_left
deleted theorem bddAbove_smul_iff_of_neg
deleted theorem bddBelow_smul_iff_of_neg
deleted theorem inv_smul_le_iff_of_neg
deleted theorem inv_smul_lt_iff_of_neg
deleted theorem lowerBounds_smul_of_neg
deleted theorem smul_inv_le_iff_of_neg
deleted theorem smul_inv_lt_iff_of_neg
deleted theorem smul_le_smul_iff_of_neg
deleted theorem smul_le_smul_of_nonpos
deleted theorem smul_lt_smul_iff_of_neg
deleted theorem smul_lt_smul_of_neg
deleted theorem smul_max_of_nonpos
deleted theorem smul_min_of_nonpos
deleted theorem smul_neg_iff_of_neg
deleted theorem smul_neg_iff_of_pos
deleted theorem smul_nonneg_iff
deleted theorem smul_nonpos_iff
deleted theorem smul_pos_iff_of_neg
deleted theorem strict_anti_smul_left
deleted theorem upperBounds_smul_of_neg
added theorem antitone_smul_left
added theorem inv_smul_le_iff_of_neg
added theorem inv_smul_lt_iff_of_neg
modified theorem neg_of_smul_neg_left
modified theorem neg_of_smul_neg_right'
modified theorem neg_of_smul_neg_right
modified theorem pos_of_smul_pos_left
modified theorem pos_of_smul_pos_right
added theorem smul_inv_le_iff_of_neg
added theorem smul_inv_lt_iff_of_neg
added theorem smul_le_smul_of_nonpos
added theorem smul_lt_smul_of_neg
added theorem smul_max_of_nonpos
added theorem smul_min_of_nonpos
added theorem smul_neg_iff_of_neg
added theorem smul_nonneg_iff
added theorem smul_nonpos_iff
added theorem smul_pos_iff_of_neg
added theorem strict_anti_smul_left