mathlib3

21b0b012 - feat(analysis/normed_space,topology/metric_space): distance between diagonal vectors (#5803)

feat(analysis/normed_space,topology/metric_space): distance between diagonal vectors (#5803) Add formulas for (e|nn|)dist between `λ _, a` and `λ _, b` as well as `∥(λ _, a)∥` and `nnnorm (λ _, a)`.