sum_dual_apply_smul_coord — Mathlib

English

The dual basis acts on a basis vector as the Kronecker delta: b.dualBasis i (b j) = δ_{ij}.

Русский

Дуальная база действует на базисный вектор как κ-дельта: b.dualBasis i (b j) = δ_{ij}.

LaTeX

$$$ b.dualBasis i (b j) = \delta_{ij}. $$$

Lean4

@[simp]
theorem sum_dual_apply_smul_coord [Fintype ι] (f : Module.Dual R M) : (∑ x, f (b x) • b.coord x) = f :=
  by
  ext m
  simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul, ← f.map_smul, ←
    map_sum, Basis.coord_apply, Basis.sum_repr]

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