Commit 2024-10-03 10:58 81d41598

View on Github →

chore: generalise more lemmas from LinearOrderedField to GroupWithZero (#17359) ... and move the lemmas from Algebra.Order.Field.Basic to Algebra.Order.GroupWithZero.Unbundled. Also take the opportunity to add ₀ at the end, per the naming convention, and to make the priming of the lemmas consistent among pairs (primes should be on the lemmas changing left multiplication into right multiplication).

Estimated changes

deleted def OrderIso.mulLeft₀
modified theorem add_div_two_lt_right
deleted theorem div_lt_comm₀
modified theorem div_lt_iff'
modified theorem div_lt_iff
modified theorem div_lt_one
deleted theorem div_self_le_one
modified theorem inv_mul_le_iff'
modified theorem inv_mul_le_iff
modified theorem inv_mul_lt_iff'
modified theorem inv_mul_lt_iff
modified theorem left_lt_add_div_two
modified theorem lt_div_iff'
modified theorem lt_div_iff
modified theorem mul_inv_le_iff'
modified theorem mul_inv_le_iff
modified theorem mul_inv_lt_iff'
modified theorem mul_inv_lt_iff
modified theorem one_lt_div
deleted theorem inv_lt_one₀
deleted theorem one_lt_inv₀
modified theorem div_le_iff₀'
added theorem div_lt_comm₀
added theorem div_lt_iff₀'
added theorem div_lt_iff₀
added theorem div_self_le_one
added theorem inv_lt_one₀
added theorem inv_mul_le_iff₀'
added theorem inv_mul_lt_iff₀'
added theorem inv_mul_lt_iff₀
added theorem inv_mul_lt_one₀
modified theorem le_div_iff₀'
added theorem le_inv_mul_iff₀'
added theorem le_mul_inv_iff₀'
added theorem lt_div_comm₀
added theorem lt_div_iff₀'
added theorem lt_div_iff₀
added theorem lt_inv_mul_iff₀'
added theorem lt_inv_mul_iff₀
added theorem lt_mul_inv_iff₀'
added theorem lt_mul_inv_iff₀
added theorem mul_inv_le_iff₀'
added theorem mul_inv_lt_iff₀'
added theorem mul_inv_lt_iff₀
added theorem one_lt_inv_mul₀
added theorem one_lt_inv₀
modified theorem NNReal.div_lt_iff'
modified theorem NNReal.div_lt_iff
added theorem NNReal.le_div_iff'
modified theorem NNReal.lt_div_iff'
modified theorem NNReal.lt_div_iff