Commit 2024-10-04 14:05 411a67a2

View on Github →

chore: generalise even more lemmas from LinearOrderedField to GroupWithZero (#17378)

Estimated changes

modified theorem div_le_of_nonneg_of_le_mul
modified theorem div_le_one_of_le
modified theorem inv_mul_le_one_of_le
modified theorem inv_pos_le_iff_one_le_mul'
modified theorem inv_pos_le_iff_one_le_mul
modified theorem inv_pos_lt_iff_one_lt_mul'
modified theorem inv_pos_lt_iff_one_lt_mul
modified theorem mul_inv_le_one_of_le
modified theorem mul_le_of_nonneg_of_le_div
added theorem div_le_of_le_mul₀
added theorem div_le_one_of_le₀
added theorem mul_le_of_le_div₀