mathlib3
7f5bf383 - move(analysis/normed/order/lattice): Move from `analysis.normed_space.lattice_ordered_group` (#17255)

Commit
3 years ago
move(analysis/normed/order/lattice): Move from `analysis.normed_space.lattice_ordered_group` (#17255) Rename `analysis.normed_space.lattice_ordered_group` to `analysis.normed.order.lattice` because it does not mention `normed_space` at all
Author
Parents
Loading