Theorem round_le_add_half

Modification history

2025-01-19 23:29
Mathlib/Algebra/Order/Floor.lean
chore(Algebra/Order/Floor): Split off `round` section (#20831) …
Modified round_le_add_halfView on Github →
2024-07-21 16:25
Mathlib/Algebra/Order/Floor.lean
feat(Order/Floor): `x - 1 / 2 < round x` (#14964) …
Added round_le_add_halfView on Github →