Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-30 10:02 3e67f50c

View on Github →

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 .

Estimated changes