Commit 2026-08-28 03:45 7c77f6d6

View on Github →

chore(Algebra/Order/Monoid/Unbundled/Basic): golfing + formatting (#38227) We make use of variable, fix some weird spacing, and golf many proofs. The only breaking change is that mul_lt_iff_lt_one_left'/add_lt_iff_neg_left now takes an explicit argument, matching the theorems surrounding it.

Estimated changes

deleted theorem Left.mul_le_one
modified theorem Left.mul_lt_mul
deleted theorem Left.mul_lt_one'
deleted theorem Left.mul_lt_one
modified theorem Left.one_le_mul
deleted theorem Left.one_lt_mul'
deleted theorem Left.one_lt_mul
modified theorem MulLECancellable.mul
deleted theorem Right.mul_le_one
modified theorem Right.mul_lt_mul
deleted theorem Right.mul_lt_one'
deleted theorem Right.mul_lt_one
deleted theorem Right.one_le_mul
deleted theorem Right.one_lt_mul'
deleted theorem Right.one_lt_mul
modified theorem le_mul_iff_one_le_left'
modified theorem le_mul_iff_one_le_right'
modified theorem le_mul_of_le_mul_left
modified theorem le_mul_of_le_mul_right
modified theorem le_mul_of_le_of_one_le
modified theorem le_mul_of_one_le_left'
modified theorem le_mul_of_one_le_of_le
modified theorem le_mul_of_one_le_right'
modified theorem le_of_le_mul_of_le_one_left
modified theorem le_of_mul_le_mul_left'
modified theorem le_of_mul_le_mul_right'
modified theorem le_of_mul_le_of_one_le_left
modified theorem le_one_of_mul_le_left
modified theorem le_one_of_mul_le_right
modified theorem lt_mul_iff_one_lt_left'
modified theorem lt_mul_iff_one_lt_right'
modified theorem lt_mul_of_le_of_one_lt
modified theorem lt_mul_of_lt_mul_left
modified theorem lt_mul_of_lt_mul_right
modified theorem lt_mul_of_lt_of_one_le
modified theorem lt_mul_of_lt_of_one_lt'
modified theorem lt_mul_of_lt_of_one_lt
modified theorem lt_mul_of_one_le_of_lt
modified theorem lt_mul_of_one_lt_left'
modified theorem lt_mul_of_one_lt_of_le
modified theorem lt_mul_of_one_lt_of_lt'
modified theorem lt_mul_of_one_lt_of_lt
modified theorem lt_mul_of_one_lt_right'
modified theorem lt_of_lt_mul_of_le_one_left
modified theorem lt_of_mul_lt_mul_left'
modified theorem lt_of_mul_lt_mul_right'
modified theorem lt_of_mul_lt_of_one_le_left
modified theorem lt_one_of_mul_lt_left
modified theorem lt_one_of_mul_lt_right
modified theorem max_mul
modified theorem min_le_max_of_mul_le_mul
modified theorem min_lt_max_of_mul_lt_mul
modified theorem min_mul
modified theorem mulLECancellable_mul
modified theorem mul_eq_one_iff_of_one_le
modified theorem mul_le_iff_le_one_left'
modified theorem mul_le_iff_le_one_right'
modified theorem mul_le_mul_iff_right
modified theorem mul_le_mul_left
modified theorem mul_le_mul_right
modified theorem mul_le_mul_three
modified theorem mul_le_of_le_of_le_one
modified theorem mul_le_of_le_one_left'
modified theorem mul_le_of_le_one_of_le
modified theorem mul_le_of_le_one_right'
modified theorem mul_le_of_mul_le_left
modified theorem mul_le_of_mul_le_right
modified theorem mul_left_inj_of_comparable
modified theorem mul_left_mono
modified theorem mul_left_strictMono
modified theorem mul_lt_iff_lt_one_left'
modified theorem mul_lt_iff_lt_one_right'
modified theorem mul_lt_mul_iff_left
modified theorem mul_lt_mul_iff_right
modified theorem mul_lt_mul_left
modified theorem mul_lt_mul_of_le_of_lt
modified theorem mul_lt_mul_of_lt_of_le
modified theorem mul_lt_mul_of_lt_of_lt
modified theorem mul_lt_mul_right
modified theorem mul_lt_of_le_of_lt_one
modified theorem mul_lt_of_le_one_of_lt
modified theorem mul_lt_of_lt_of_le_one
modified theorem mul_lt_of_lt_of_lt_one'
modified theorem mul_lt_of_lt_of_lt_one
modified theorem mul_lt_of_lt_one_left'
modified theorem mul_lt_of_lt_one_of_le
modified theorem mul_lt_of_lt_one_of_lt'
modified theorem mul_lt_of_lt_one_of_lt
modified theorem mul_lt_of_lt_one_right'
modified theorem mul_lt_of_mul_lt_left
modified theorem mul_lt_of_mul_lt_right
modified theorem mul_max
modified theorem mul_min
modified theorem mul_right_inj_of_comparable
modified theorem mul_right_mono
modified theorem mul_right_strictMono
modified theorem one_le_of_le_mul_left
modified theorem one_le_of_le_mul_right
modified theorem one_lt_of_lt_mul_left
modified theorem one_lt_of_lt_mul_right
modified theorem trichotomy_of_mul_eq_mul