Theorem div_nat_lt_self_of_pos_of_two_le

Modification history

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