Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 13:20 f238733a

View on Github →

feat(algebra/order/smul): Monotonicity of scalar multiplication (#9558) Also prove smul_nonneg, smul_pos and variants.

Estimated changes

Modified src/algebra/module/ordered.lean

added theorem antitone_smul_left

added def order_iso.smul_left_dual

added theorem smul_nonneg_of_nonpos_of_nonpos

added theorem smul_nonpos_of_nonpos_of_nonneg

added theorem strict_anti_smul_left

Modified src/algebra/order/smul.lean

added theorem monotone_smul_left

added theorem order_dual.of_dual_smul

added theorem order_dual.to_dual_smul

added def order_iso.smul_left

added theorem smul_nonneg

added theorem smul_nonpos_of_nonneg_of_nonpos

added theorem strict_mono_smul_left