coe_repr_symm — Mathlib

English

The inverse coordinate map corresponds to the linear combination operator: the map b.repr.symm is equal to the linear combination operator with respect to b.

Русский

Обратная координатная карта совпадает с операцией линейной комбинации по базису; b.repr.symm = Finsupp.linearCombination b.

LaTeX

$$$\uparrow b.\mathrm{repr}^{-1} = \mathrm{Finsupp}.linearCombination(R, b)$$$

Lean4

@[simp]
theorem coe_repr_symm : ↑b.repr.symm = Finsupp.linearCombination R b :=
  LinearMap.ext fun v => b.repr_symm_apply v

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