mathlib

76ec0e53 - move(analysis/normed/order/basic): Move from `analysis.normed_space.ordered` (#17239)

move(analysis/normed/order/basic): Move from `analysis.normed_space.ordered` (#17239) Rename `analysis.normed_space.ordered` to `analysis.normed.order.basic` because: * It wasn't mentioning `normed_space` at all * I am about to add properties of upper/lower sets in normed ordered groups