mathlib3
03ed4c78 - move(topology/algebra/floor_ring → order/floor): Move topological properties of `⌊x⌋` and `⌈x⌉` (#13824)

Commit
3 years ago
move(topology/algebra/floor_ring → order/floor): Move topological properties of `⌊x⌋` and `⌈x⌉` (#13824) Those belong in an order folder.
Author
Parents
Loading