Commit 2023-01-16 20:07 4d566e7f

View on Github →

feat: port Algebra.Order.SMul (#1553)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/SMul.lean

added theorem BddAbove.smul_of_nonneg

added theorem BddBelow.smul_of_nonneg

added def OrderIso.smulLeft

added theorem OrderedSMul.mk''

added theorem OrderedSMul.mk'

added theorem bddAbove_smul_iff_of_pos

added theorem bddBelow_smul_iff_of_pos

added theorem eq_of_smul_eq_smul_of_pos_of_le

added theorem inv_smul_le_iff

added theorem inv_smul_lt_iff

added theorem le_inv_smul_iff

added theorem lowerBounds_smul_of_pos

added theorem lt_inv_smul_iff

added theorem lt_of_smul_lt_smul_of_nonneg

added theorem monotone_smul_left

added theorem smul_le_smul_iff_of_pos

added theorem smul_le_smul_of_nonneg

added theorem smul_lowerBounds_subset_lowerBounds_smul

added theorem smul_lt_smul_iff_of_pos

added theorem smul_lt_smul_of_pos

added theorem smul_nonneg

added theorem smul_nonpos_of_nonneg_of_nonpos

added theorem smul_pos_iff_of_pos

added theorem smul_upperBounds_subset_upperBounds_smul

added theorem strictMono_smul_left

added theorem upperBounds_smul_of_pos