Commit 2024-10-11 15:01 683a462b

View on Github →

chore: generalise zpow lemmas from LinearOrderedSemifield to GroupWithZero (#17539)

Estimated changes

modified theorem one_lt_zpow
modified theorem zpow_injective
modified theorem zpow_le_of_le
modified theorem inv_le_one_iff₀
modified theorem inv_lt_one_iff₀
added theorem one_le_zpow₀
added theorem one_lt_zpow_of_neg₀
added theorem one_lt_zpow₀
added theorem zpow_le_one₀
added theorem zpow_le_zpow_right₀
added theorem zpow_lt_one_of_neg₀
added theorem zpow_lt_one₀
added theorem zpow_lt_zpow_right₀
added theorem zpow_pos
deleted theorem zpow_pos_of_pos
added theorem zpow_right_anti₀
added theorem zpow_right_inj₀
added theorem zpow_right_mono₀
deleted theorem NNReal.zpow_pos