Commit 2024-11-13 17:52 798302c5

View on Github →

chore: rename zpow monotonicity lemmas (#18956) These new names match the ones introduced in the analogous PR #9095

Estimated changes

deleted theorem one_lt_zpow
deleted theorem one_lt_zpow'
added theorem one_lt_zpow
deleted theorem zpow_le_zpow'
deleted theorem zpow_le_zpow
deleted theorem zpow_le_zpow_iff'
deleted theorem zpow_le_zpow_iff
added theorem zpow_le_zpow_iff_left
added theorem zpow_le_zpow_iff_right
added theorem zpow_le_zpow_left
added theorem zpow_le_zpow_right
added theorem zpow_left_mono
added theorem zpow_left_strictMono
deleted theorem zpow_lt_zpow'
deleted theorem zpow_lt_zpow
deleted theorem zpow_lt_zpow_iff'
deleted theorem zpow_lt_zpow_iff
added theorem zpow_lt_zpow_iff_left
added theorem zpow_lt_zpow_iff_right
added theorem zpow_lt_zpow_left
added theorem zpow_lt_zpow_right
deleted theorem zpow_mono_left
deleted theorem zpow_mono_right
added theorem zpow_right_mono
deleted theorem zpow_strictMono_left