repr_sum_self — Mathlib

English

For any function c: ι → R, the representation of the vector ∑ i c(i) b_i equals c(i) at each i: b.repr (∑ i, c i • b i) = c.

Русский

Для любой функции c: ι → R представление вектора ∑_i c(i) b_i равно c на каждой позиции: b.repr (∑ i c_i b_i) = c.

LaTeX

$$$$ b.repr\left(\sum_i c_i \cdot b_i\right) = c $$$$

Lean4

theorem repr_sum_self [Fintype ι] (b : Basis ι R M) (c : ι → R) : b.repr (∑ i, c i • b i) = c := by
  simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

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