English
For a finite index type, a linear map f on the Pi-space satisfies the basis expansion: f x = ∑ i, x_i • f e_i, where e_i is the i-th canonical basis vector.
Русский
Для конечного множества индексов линейное отображение f на произведении функций раскладывается по базису: f x = ∑_i x_i f e_i, где e_i — i-й канонический базисный вектор.
LaTeX
$$$$f\\,x = \\sum_i x_i\\, f\\,e_i,$$$$
Lean4
/-- A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements
of the canonical basis. -/
theorem pi_apply_eq_sum_univ [Fintype ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R) :
f x = ∑ i, x i • f fun j => if i = j then 1 else 0 :=
by
conv_lhs => rw [pi_eq_sum_univ x, map_sum]
refine Finset.sum_congr rfl (fun _ _ => ?_)
rw [map_smul]
