Commit 2024-06-06 18:43 4411c7e9

View on Github →

chore: Split Algebra.GroupPower.Order (#12964) Move its lemmas (mostly) to two new files:

  • Algebra.Order.Group.Basic for the lemmas about group-like objects
  • Algebra.Order.Ring.Basic for the lemmas about ring-like objects

Estimated changes

added theorem one_lt_zpow'
added theorem zpow_eq_zpow_iff'
added theorem zpow_le_zpow'
added theorem zpow_le_zpow
added theorem zpow_le_zpow_iff'
added theorem zpow_le_zpow_iff
added theorem zpow_left_inj
added theorem zpow_left_injective
added theorem zpow_lt_zpow'
added theorem zpow_lt_zpow
added theorem zpow_lt_zpow_iff'
added theorem zpow_lt_zpow_iff
added theorem zpow_mono_left
added theorem zpow_mono_right
added theorem zpow_right_strictMono
added theorem zpow_strictMono_left
added theorem StrictMono.nat_pow
deleted theorem StrictMono.nat_pow
deleted theorem one_lt_zpow'
deleted theorem zpow_eq_zpow_iff'
deleted theorem zpow_le_zpow'
deleted theorem zpow_le_zpow
deleted theorem zpow_le_zpow_iff'
deleted theorem zpow_le_zpow_iff
deleted theorem zpow_left_inj
deleted theorem zpow_left_injective
deleted theorem zpow_lt_zpow'
deleted theorem zpow_lt_zpow
deleted theorem zpow_lt_zpow_iff'
deleted theorem zpow_lt_zpow_iff
deleted theorem zpow_mono_left
deleted theorem zpow_mono_right
deleted theorem zpow_right_strictMono
deleted theorem zpow_strictMono_left