Commit 2023-12-18 07:15 d61c95e1

View on Github →

chore: Rename pow monotonicity lemmas (#9095) The names for lemmas about monotonicity of (a ^ ·) and (· ^ n) were a mess. This PR tidies up everything related by following the naming convention for (a * ·) and (· * b). Namely, (a ^ ·) is pow_right and (· ^ n) is pow_left in lemma names. All lemma renames follow the corresponding multiplication lemma names closely.

Renames

Algebra.GroupPower.Order

  • pow_monopow_right_mono
  • pow_le_powpow_le_pow_right
  • pow_le_pow_of_le_leftpow_le_pow_left
  • pow_lt_pow_of_lt_leftpow_lt_pow_left
  • strictMonoOn_powpow_left_strictMonoOn
  • pow_strictMono_rightpow_right_strictMono
  • pow_lt_powpow_lt_pow_right
  • pow_lt_pow_iffpow_lt_pow_iff_right
  • pow_le_pow_iffpow_le_pow_iff_right
  • self_lt_powlt_self_pow
  • strictAnti_powpow_right_strictAnti
  • pow_lt_pow_iff_of_lt_onepow_lt_pow_iff_right_of_lt_one
  • pow_lt_pow_of_lt_onepow_lt_pow_right_of_lt_one
  • lt_of_pow_lt_powlt_of_pow_lt_pow_left
  • le_of_pow_le_powle_of_pow_le_pow_left
  • pow_lt_pow₀pow_lt_pow_right₀

Algebra.GroupPower.CovariantClass

  • pow_le_pow_of_le_left'pow_le_pow_left'
  • nsmul_le_nsmul_of_le_rightnsmul_le_nsmul_right
  • pow_lt_pow'pow_lt_pow_right'
  • nsmul_lt_nsmulnsmul_lt_nsmul_left
  • pow_strictMono_leftpow_right_strictMono'
  • nsmul_strictMono_rightnsmul_left_strictMono
  • StrictMono.pow_right'StrictMono.pow_const
  • StrictMono.nsmul_leftStrictMono.const_nsmul
  • pow_strictMono_right'pow_left_strictMono
  • nsmul_strictMono_leftnsmul_right_strictMono
  • Monotone.pow_rightMonotone.pow_const
  • Monotone.nsmul_leftMonotone.const_nsmul
  • lt_of_pow_lt_pow'lt_of_pow_lt_pow_left'
  • lt_of_nsmul_lt_nsmullt_of_nsmul_lt_nsmul_right
  • pow_le_pow'pow_le_pow_right'
  • nsmul_le_nsmulnsmul_le_nsmul_left
  • pow_le_pow_of_le_one'pow_le_pow_right_of_le_one'
  • nsmul_le_nsmul_of_nonposnsmul_le_nsmul_left_of_nonpos
  • le_of_pow_le_pow'le_of_pow_le_pow_left'
  • le_of_nsmul_le_nsmul'le_of_nsmul_le_nsmul_right'
  • pow_le_pow_iff'pow_le_pow_iff_right'
  • nsmul_le_nsmul_iffnsmul_le_nsmul_iff_left
  • pow_lt_pow_iff'pow_lt_pow_iff_right'
  • nsmul_lt_nsmul_iffnsmul_lt_nsmul_iff_left

Data.Nat.Pow

  • Nat.pow_lt_pow_of_lt_leftNat.pow_lt_pow_left
  • Nat.pow_le_iff_le_leftNat.pow_le_pow_iff_left
  • Nat.pow_lt_iff_lt_leftNat.pow_lt_pow_iff_left

Lemmas added

  • pow_le_pow_iff_left
  • pow_lt_pow_iff_left
  • pow_right_injective
  • pow_right_inj
  • Nat.pow_le_pow_left to have the correct name since Nat.pow_le_pow_of_le_left is in Std.
  • Nat.pow_le_pow_right to have the correct name since Nat.pow_le_pow_of_le_right is in Std.

Lemmas removed

  • self_le_pow was a duplicate of le_self_pow.
  • Nat.pow_lt_pow_of_lt_right is defeq to pow_lt_pow_right.
  • Nat.pow_right_strictMono is defeq to pow_right_strictMono.
  • Nat.pow_le_iff_le_right is defeq to pow_le_pow_iff_right.
  • Nat.pow_lt_iff_lt_right is defeq to pow_lt_pow_iff_right.

Other changes

  • A bunch of proofs have been golfed.
  • Some lemma assumptions have been turned from 0 < n or 1 ≤ n to n ≠ 0.
  • A few Nat lemmas have been protected.
  • One docstring has been fixed.

Estimated changes

added theorem StrictMono.pow_const
deleted theorem StrictMono.pow_right'
deleted theorem le_of_pow_le_pow'
added theorem le_of_pow_le_pow_left'
deleted theorem lt_of_pow_lt_pow'
added theorem lt_of_pow_lt_pow_left'
deleted theorem pow_le_pow'
deleted theorem pow_le_pow_iff'
added theorem pow_le_pow_iff_right'
added theorem pow_le_pow_left'
deleted theorem pow_le_pow_of_le_left'
deleted theorem pow_le_pow_of_le_one'
added theorem pow_le_pow_right'
added theorem pow_left_strictMono
deleted theorem pow_lt_pow'
deleted theorem pow_lt_pow_iff'
added theorem pow_lt_pow_iff_right'
added theorem pow_lt_pow_right'
added theorem pow_right_strictMono'
deleted theorem pow_strictMono_left
deleted theorem pow_strictMono_right'
modified theorem abs_pow_eq_one
deleted theorem le_of_pow_le_pow
added theorem le_of_pow_le_pow_left
modified theorem le_self_pow
deleted theorem lt_of_pow_lt_pow
added theorem lt_of_pow_lt_pow_left
added theorem lt_self_pow
modified theorem one_le_pow_iff_of_nonneg
modified theorem one_lt_pow_iff_of_nonneg
modified theorem pow_eq_one_iff_of_nonneg
modified theorem pow_le_one_iff_of_nonneg
deleted theorem pow_le_pow
deleted theorem pow_le_pow_iff
added theorem pow_le_pow_iff_left
added theorem pow_le_pow_iff_right
added theorem pow_le_pow_left
deleted theorem pow_le_pow_of_le_left
added theorem pow_le_pow_right
modified theorem pow_left_inj
added theorem pow_left_strictMonoOn
modified theorem pow_lt_one_iff_of_nonneg
deleted theorem pow_lt_pow
deleted theorem pow_lt_pow_iff
added theorem pow_lt_pow_iff_left
deleted theorem pow_lt_pow_iff_of_lt_one
added theorem pow_lt_pow_iff_right
added theorem pow_lt_pow_left
deleted theorem pow_lt_pow_of_lt_left
deleted theorem pow_lt_pow_of_lt_one
added theorem pow_lt_pow_right
added theorem pow_lt_pow_right₀
deleted theorem pow_lt_pow₀
modified theorem pow_lt_self_of_lt_one
deleted theorem pow_mono
added theorem pow_right_inj
added theorem pow_right_injective
added theorem pow_right_mono
added theorem pow_right_strictAnti
added theorem pow_right_strictMono
deleted theorem pow_strictMono_right
deleted theorem self_le_pow
deleted theorem self_lt_pow
deleted theorem strictAnti_pow
deleted theorem strictMonoOn_pow
modified theorem Nat.one_lt_pow
modified theorem Nat.one_lt_pow_iff
modified theorem Nat.one_lt_two_pow
deleted theorem Nat.pow_le_iff_le_left
deleted theorem Nat.pow_le_iff_le_right
modified theorem Nat.pow_left_injective
deleted theorem Nat.pow_left_strictMono
deleted theorem Nat.pow_lt_iff_lt_left
deleted theorem Nat.pow_lt_iff_lt_right
deleted theorem Nat.pow_lt_pow_of_lt_left
deleted theorem Nat.pow_right_injective
deleted theorem Nat.pow_right_strictMono
modified theorem StrictMono.nat_pow