Mathlib v3 is deprecated. Go to Mathlib v4

Theorem round_one

Modification history

2022-08-25 18:07

src/algebra/order/floor.lean

feat(algebra/order/floor): lemmas about `int.floor`, `int.ceil`, `int.fract`, `round` (#16158)

Modified round_one View on Github →

2022-07-15 15:49

src/algebra/order/archimedean.lean

chore(algebra/order/archimedean): Move material to correct files (#15290) …

Modified round_one View on Github →

2021-05-03 17:06

src/algebra/archimedean.lean

chore(*): update to lean 3.30.0c (#7264) …

Added round_one View on Github →