coe_complexBasis — Mathlib

English

The coefficient map of the complex basis equals the identity on AddChar α ℂ.

Русский

Коэффициентная карта комплексной базы равна тождественному отображению на AddChar α ℂ.

LaTeX

$$$ \text{coe_complexBasis} : ∀ ψ, \text{complexBasis}(α)(ψ) = ψ $$$

Lean4

@[simp, norm_cast]
theorem coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ) := by
  rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]

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