Theorem one_lt_zpow
Modification history
2025-07-07 17:19
Mathlib/Algebra/Order/Group/Basic.lean
feat: `(· ^ n)` is strictly monotone on nonnegative inputs for `n : ℤ` (#26762) …
Modified one_lt_zpowView on Github →2024-11-13 17:52
Mathlib/Algebra/Order/Field/Power.lean
chore: rename zpow monotonicity lemmas (#18956) …
Modified one_lt_zpowView on Github →