Commit 2023-02-11 06:32 7e81ebff

View on Github →

feat: port Algebra.Order.Module (#1573)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Module.lean

added theorem BddAbove.smul_of_nonpos

added theorem BddBelow.smul_of_nonpos

added def OrderIso.smulLeftDual

added theorem antitone_smul_left

added theorem bddAbove_smul_iff_of_neg

added theorem bddBelow_smul_iff_of_neg

added theorem eq_of_smul_eq_smul_of_neg_of_le

added theorem inv_smul_le_iff_of_neg

added theorem inv_smul_lt_iff_of_neg

added theorem lowerBounds_smul_of_neg

added theorem lt_of_smul_lt_smul_of_nonpos

added theorem smul_add_smul_le_smul_add_smul'

added theorem smul_add_smul_le_smul_add_smul

added theorem smul_add_smul_lt_smul_add_smul'

added theorem smul_add_smul_lt_smul_add_smul

added theorem smul_inv_le_iff_of_neg

added theorem smul_inv_lt_iff_of_neg

added theorem smul_le_smul_iff_of_neg

added theorem smul_le_smul_of_nonpos

added theorem smul_lowerBounds_subset_upperBounds_smul

added theorem smul_lt_smul_iff_of_neg

added theorem smul_lt_smul_of_neg

added theorem smul_neg_iff_of_neg

added theorem smul_neg_iff_of_pos

added theorem smul_nonneg_of_nonpos_of_nonpos

added theorem smul_nonpos_of_nonpos_of_nonneg

added theorem smul_pos_iff_of_neg

added theorem smul_upperBounds_subset_lowerBounds_smul

added theorem strict_anti_smul_left

added theorem upperBounds_smul_of_neg