Theorem one_lt_div₀

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 one_lt_div₀View on Github →