basisOneI — Mathlib

English

The complex numbers form a real vector space basis {1, i}.

Русский

Комплексные числа как вещественное пространство имеют базис {1, i}.

LaTeX

$$$\\\\text{basisOneI} = \\\\{1, i\\\\}$$$

Lean4

/-- `ℂ` has a basis over `ℝ` given by `1` and `I`. -/
noncomputable def basisOneI : Basis (Fin 2) ℝ ℂ :=
  .ofEquivFun
    { toFun := fun z => ![z.re, z.im]
      invFun := fun c => c 0 + c 1 • I
      left_inv := fun z => by simp
      right_inv := fun c => by
        ext i
        fin_cases i <;> simp
      map_add' := fun z z' => by simp
      map_smul' := fun c z => by simp }

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