Theorem round_one

Modification history

2025-01-19 23:29

Mathlib/Algebra/Order/Floor.lean

chore(Algebra/Order/Floor): Split off `round` section (#20831) …

Modified round_one View on Github →

2023-01-10 17:53

Mathlib/Algebra/Order/Floor.lean

feat: port `Algebra.Order.Floor` (#1304) …

Added round_one View on Github →