Theorem Nat.one_le_cast_iff_ne_zero

Modification history

2025-07-07 17:19
Mathlib/Data/Nat/Cast/Order/Basic.lean
feat(Algebra): `a / n ≤ a` if `n : ℕ` and `0 ≤ a` (#26658) …
Added Nat.one_le_cast_iff_ne_zeroView on Github →