Theorem div_lt_one₀

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