coe_basisOneI — Mathlib

English

The coordinate map for basisOneI sends z to its coordinate vector [z.re, z.im].

Русский

Координатное отображение basisOneI отправляет z в вектор координат [z.re, z.im].

LaTeX

$$$\\\\forall z \\\\in \\\\mathbb{C}, \\\\big[\\\\operatorname{basisOneI.repr} (z)\\\\big] = [z_{re}, z_{im}]$$$

Lean4

@[simp]
theorem coe_basisOneI : ⇑basisOneI = ![1, I] :=
  funext fun i => Basis.apply_eq_iff.mpr <| Finsupp.ext fun j => by fin_cases i <;> fin_cases j <;> simp

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