repr_linearCombination

Mathlib.LinearAlgebra.Basis.Defs

URI: https://scilib.ai/kg/mathlib#Module.Basis.repr_linearCombination

← MathLib Explorer

English

For any v, the representation of the linear combination ∑_i v_i · b_i is v itself.

Русский

Для любого v представление линейной комбинации ∑_i v_i b_i равно самому v.

LaTeX

$$$\mathrm{repr}(\sum_i v_i \cdot b_i) = v$$$

Lean4

@[simp]
theorem repr_linearCombination (v) : b.repr (Finsupp.linearCombination _ b v) = v :=
  by
  rw [← b.coe_repr_symm]
  exact b.repr.apply_symm_apply v

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru