Theorem zpow_lt_zpow_iff_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) …
Added zpow_lt_zpow_iff_right_of_lt_one₀View on Github →