Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 19:54 158fbc5d

View on Github →

refactor(algebra/module/order): Make space argument explicit in the order_iso (#9706) Explicitly providing M in order_iso.smul_left and order_iso.smul_left_dual turns out to work much better with dot notation on order_iso. This allows golfing half the proofs introduced in #9078.

Estimated changes

modified theorem bdd_above.smul_of_nonneg
modified theorem bdd_above.smul_of_nonpos
modified theorem bdd_above_smul_iff_of_neg
modified theorem bdd_above_smul_iff_of_pos
modified theorem bdd_below.smul_of_nonneg
modified theorem bdd_below.smul_of_nonpos
modified theorem bdd_below_smul_iff_of_neg
modified theorem bdd_below_smul_iff_of_pos
modified theorem lower_bounds_smul_of_neg
modified theorem lower_bounds_smul_of_pos
modified theorem upper_bounds_smul_of_neg
modified theorem upper_bounds_smul_of_pos