Theorem zpow_left_strictMonoOn₀

Modification history

2025-07-07 17:19
Mathlib/Algebra/Order/GroupWithZero/Unbundled/Basic.lean
feat: `(· ^ n)` is strictly monotone on nonnegative inputs for `n : ℤ` (#26762) …
Added zpow_left_strictMonoOn₀View on Github →