mathlib3
d6b861b0 - chore(algebra/order/archimedean): Move material to correct files (#15290)

Commit
3 years ago
chore(algebra/order/archimedean): Move material to correct files (#15290) Move `round` and some `floor` lemmas to `algebra.order.floor`. Move the `rat.cast` lemmas about `floor` and `ceil` to `data.rat.floor`. Merge a few sections together now that unrelated lemmas are gone.
Author
Parents
Loading