mathlib
1b5f8c28 - chore(topology/algebra/ordered/*): Rename folder (#11988)

Commit
3 years ago
chore(topology/algebra/ordered/*): Rename folder (#11988) Rename `topology.algebra.ordered` to `topology.algebra.order` to match `order`, `algebra.order`, `topology.order`.
Author
Parents
Loading