Commit 2025-04-24 20:04 8ca285ce

View on Github →

chore(Algebra/Order/GroupWithZero): review (#24301) Reorder lemmas, unify assumptions, generalize from LinearOrder to PartialOrder. Lemmas in this file used to have many different sets of typeclass assumptions, so they were sorted according to the assumptions. Recently, I've reduced the number of sets of assumptions, but didn't reorder the lemmas. In this PR, I further unify assumptions and reorder theorems.

Estimated changes

modified theorem Set.image_affine_Icc'
modified theorem Set.image_affine_Ico
modified theorem Set.image_affine_Ioc
modified theorem Set.image_affine_Ioo
added theorem Right.inv_nonneg
modified theorem div_le_div_iff_of_pos_left
modified theorem div_le_div_iff_of_pos_right
modified theorem div_lt_div_iff_of_pos_left
modified theorem div_lt_div_iff_of_pos_right
modified theorem div_lt_div_of_pos_left
modified theorem inv_le_one_of_one_le₀
modified theorem inv_mul_le_iff₀
modified theorem inv_mul_lt_iff₀
modified theorem le_inv_mul_iff₀
modified theorem le_mul_inv_iff₀
modified theorem lt_inv_mul_iff₀
modified theorem lt_mul_inv_iff₀
modified theorem mul_inv_le_iff₀
modified theorem mul_inv_lt_iff₀
modified theorem one_le_inv_iff₀
modified theorem zpow_nonneg
modified theorem zpow_pos