Commit 2024-10-08 18:09 b5a8246b

View on Github →

chore: generalise yet more lemmas from LinearOrderedField to GroupWithZero (#17447)

Estimated changes

modified theorem inv_le
modified theorem inv_le_inv
modified theorem inv_le_inv_of_le
modified theorem inv_le_of_inv_le
modified theorem inv_le_one
modified theorem inv_le_one_iff
modified theorem inv_lt
modified theorem inv_lt_inv
modified theorem inv_lt_inv_of_lt
modified theorem inv_lt_of_inv_lt
modified theorem inv_lt_one
modified theorem inv_lt_one_iff
modified theorem inv_lt_one_iff_of_pos
modified theorem le_inv
modified theorem le_one_div
modified theorem lt_inv
modified theorem lt_one_div
modified theorem one_div_le
modified theorem one_div_lt
modified theorem one_le_inv
modified theorem one_le_inv_iff
modified theorem one_lt_inv
modified theorem one_lt_inv_iff
deleted theorem inv_le_inv₀
deleted theorem inv_lt_inv₀
added theorem inv_anti₀
added theorem inv_le_comm₀
added theorem inv_le_inv₀
added theorem inv_le_of_inv_le₀
added theorem inv_le_one_iff₀
added theorem inv_lt_comm₀
added theorem inv_lt_inv₀
added theorem inv_lt_of_inv_lt₀
added theorem inv_lt_one_iff₀
added theorem inv_strictAnti₀
added theorem le_inv_comm₀
added theorem le_inv_of_le_inv₀
added theorem lt_inv_comm₀
added theorem lt_inv_of_lt_inv₀
added theorem one_le_inv_iff₀
added theorem one_lt_inv_iff₀
modified theorem midpoint_le_right
modified theorem right_le_midpoint
added theorem Valuation.pos_iff