Commit 2024-08-26 13:45 9295e9f3

View on Github →

refactor: Generalise ordered field lemmas to ordered groups with zero (#16036) Also generalise LinearOrderedCommGroupWithZero lemmas, add a few missing ones and unify the names. Note that this doesn't generalise all eligible lemmas as there are too many for a single PR. Unify:

  • le_div_iff → le_div_iff₀
  • le_div_iff' → le_div_iff₀'
  • div_le_iff → div_le_iff₀
  • div_le_iff' → div_le_iff₀'
  • mul_le_one₀ → mul_le_one'
  • one_le_mul₀ → one_le_mul' From LeanAPAP

Estimated changes

deleted theorem div_le_comm₀
deleted theorem div_le_iff'
deleted theorem div_le_iff
modified theorem div_le_one
deleted theorem le_div_iff'
deleted theorem le_div_iff
modified theorem one_le_div
deleted theorem div_nonneg
deleted theorem div_pos
deleted theorem inv_lt_zero
deleted theorem inv_nonneg
deleted theorem inv_nonpos
deleted theorem inv_pos
deleted theorem one_div_neg
deleted theorem one_div_nonneg
deleted theorem one_div_nonpos
deleted theorem one_div_pos
deleted theorem zpow_nonneg
deleted theorem zpow_pos_of_pos
deleted theorem div_le_div₀
deleted theorem div_le_iff₀
deleted theorem inv_le_one₀
deleted theorem le_div_iff₀
deleted theorem le_mul_inv_iff₀
modified theorem le_of_le_mul_right
deleted theorem mul_inv_le_iff₀
modified theorem mul_le_mul_left₀
modified theorem mul_lt_right₀
deleted theorem one_le_inv₀
added theorem Antitone.const_mul
added theorem Antitone.mul_const
added theorem Monotone.const_mul
added theorem Monotone.mul
added theorem Monotone.mul_const
added theorem StrictAnti.const_mul
added theorem StrictAnti.mul_const
added theorem StrictMono.const_mul
added theorem StrictMono.mul
added theorem StrictMono.mul_const
added theorem div_le_comm₀
added theorem div_le_div₀
added theorem div_le_iff₀'
added theorem div_le_iff₀
added theorem div_le_one₀
added theorem div_nonneg
added theorem div_pos
added theorem inv_le_one₀
added theorem inv_mul_le_iff₀
added theorem inv_mul_le_one₀
added theorem inv_neg''
added theorem inv_nonneg
added theorem inv_nonpos
added theorem inv_pos
added theorem le_div_comm₀
added theorem le_div_iff₀'
added theorem le_div_iff₀
added theorem le_inv_mul_iff₀
added theorem le_mul_inv_iff₀
added theorem lt_mul_left
added theorem lt_mul_right
added theorem lt_mul_self
added theorem mul_inv_le_iff₀
added theorem mul_le_one
added theorem mul_self_lt_mul_self
added theorem one_div_neg
added theorem one_div_nonneg
added theorem one_div_nonpos
added theorem one_div_pos
added theorem one_le_div₀
added theorem one_le_inv_mul₀
added theorem one_le_inv₀
added theorem one_lt_mul_of_le_of_lt
added theorem one_lt_mul_of_lt_of_le
added theorem pow_le_of_le_one
added theorem pow_le_pow_of_le_one
added theorem pow_nonneg
added theorem pow_pos
added theorem sq_le
added theorem strictMonoOn_mul_self
added theorem zpow_nonneg
added theorem zpow_pos_of_pos
deleted theorem Antitone.const_mul
deleted theorem Antitone.mul_const
deleted theorem Monotone.const_mul
deleted theorem Monotone.mul
deleted theorem Monotone.mul_const
deleted theorem Monotone.mul_strictMono
deleted theorem StrictAnti.const_mul
deleted theorem StrictAnti.mul_const
deleted theorem StrictMono.const_mul
deleted theorem StrictMono.mul
deleted theorem StrictMono.mul_const
deleted theorem StrictMono.mul_monotone
deleted theorem lt_mul_left
deleted theorem lt_mul_right
deleted theorem lt_mul_self
deleted theorem mul_le_one
deleted theorem mul_self_lt_mul_self
deleted theorem one_lt_mul_of_le_of_lt
deleted theorem one_lt_mul_of_lt_of_le
deleted theorem pow_le_of_le_one
deleted theorem pow_le_pow_of_le_one
deleted theorem pow_nonneg
deleted theorem pow_pos
deleted theorem sq_le
deleted theorem strictMonoOn_mul_self
deleted theorem NNReal.div_le_iff
modified theorem NNReal.mul_le_iff_le_inv