repr_symm_apply — Mathlib

English

For any vector v in the coordinate space, b.repr^{-1}(v) equals the finite sum ∑_i v_i · b_i.

Русский

Для вектора v в координатном пространстве, b.repr^{-1}(v) = ∑_i v_i · b_i.

LaTeX

$$$b.\mathrm{repr}^{-1}(v) = \sum_i v_i \cdot b_i$$$

Lean4

@[simp]
theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.linearCombination R b v :=
  calc
    b.repr.symm v = b.repr.symm (v.sum Finsupp.single) := by simp
    _ = v.sum fun i vi => b.repr.symm (Finsupp.single i vi) := map_finsuppSum ..
    _ = Finsupp.linearCombination R b v := by simp only [repr_symm_single, Finsupp.linearCombination_apply]

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