Commit 2024-11-20 10:54 e69c3062

View on Github →

chore: deprecate LinearOrderedCommGroupWithZero lemmas (#19197) Deprecate almost all lemmas about LinearOrderedCommGroupWithZero and remove three months old deprecations.

Estimated changes

modified def OrderIso.mulLeft₀'
modified def OrderIso.mulRight₀'
modified theorem div_le_div_left₀
modified theorem div_le_div_right₀
deleted theorem le_mul_inv_of_mul_le
deleted theorem le_of_le_mul_right
modified theorem mul_inv_le_of_le_mul
deleted theorem mul_le_mul_left₀
deleted theorem mul_le_mul_right₀
deleted theorem mul_lt_right₀
deleted theorem one_le_mul₀
modified theorem pow_lt_pow_succ
modified def OrderIso.divRight₀
modified def OrderIso.mulLeft₀
modified def OrderIso.mulRight₀