linearCombination_repr — Mathlib

English

The equality of the two ways to form v from its coordinates via the basis is encoded by linearCombination.

Русский

Эквивалентность двух способов получить вектор по координатам через базис задаётся линейной комбинацией.

LaTeX

$$$\mathrm{repr\_linearCombination}(b, v) = v$$$

Lean4

@[simp]
theorem linearCombination_repr : Finsupp.linearCombination _ b (b.repr x) = x :=
  by
  rw [← b.coe_repr_symm]
  exact b.repr.symm_apply_apply x

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