orthonormalBasisOneI — Mathlib

English

As a real inner product space, the complex numbers C admit the orthonormal basis formed by 1 and i.

Русский

Как вещественное евклидово пространство, множество комплексных чисел C имеет ортонормированный базис, состоящий из 1 и i.

LaTeX

$$$\{1,i\}$ is an orthonormal basis of $\mathbb{C}$ as a real inner product space.$$

Lean4

/-- `![1, I]` is an orthonormal basis for `ℂ` considered as a real inner product space. -/
def orthonormalBasisOneI : OrthonormalBasis (Fin 2) ℝ ℂ :=
  Complex.basisOneI.toOrthonormalBasis
    (by
      rw [orthonormal_iff_ite]
      intro i; fin_cases i <;> intro j <;> fin_cases j <;> simp [real_inner_eq_re_inner])

Похожие утверждения