Commit 2021-03-30 10:02 3e67f50c

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 ℂ.