linear_combination_coord_eq_self — Mathlib

English

In the module case, every vector v ∈ V can be recovered from its coordinates by a finite linear combination of the basis vectors: v = ∑_{i} coord_i(v) · b_i.

Русский

В случае модуля каждый вектор v можно восстановить из координат: v = ∑_{i} coord_i(v) · b_i.

LaTeX

$$$\\sum_{i \\in \\text{Finset.univ}} b.coord\\, i\\; v \\cdot b_i = v$$$

Lean4

/-- A variant of `AffineBasis.affineCombination_coord_eq_self` for the special case when the
affine space is a module so we can talk about linear combinations. -/
@[simp]
theorem linear_combination_coord_eq_self [Fintype ι] (b : AffineBasis ι k V) (v : V) : ∑ i, b.coord i v • b i = v :=
  by
  have hb := b.affineCombination_coord_eq_self v
  rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb

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