mathlib

3e67f50c - feat(analysis/normed_space/inner_product): isometry of ℂ with Euclidean space (#6877)

feat(analysis/normed_space/inner_product): isometry of ℂ with Euclidean space (#6877) `ℂ` is isometric to `fin 2 → ℝ` with the Euclidean inner product. The isometry given here is that defined by the ordered basis {1, i} for `ℂ`.