Theorem sub_half_lt_round

Modification history

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