Theorem zpow_lt_zpow_right_of_lt_one₀

Modification history

2024-10-21 14:11
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
feat: `a ^ n = 1 ↔ n = 0` and similar (#17745) …
Modified zpow_lt_zpow_right_of_lt_one₀View on Github →
2024-10-11 15:01
Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)
Added zpow_lt_zpow_right_of_lt_one₀View on Github →