English
Let f be a finitely supported function f: ι → R. Then the dual evaluated at the linear combination Finsupp.linearCombination R b f satisfies b.toDual(Finsupp.linearCombination R b f)(b_i) = f_i for each i.
Русский
Пусть f: ι →₀ R конечно-допускается. Тогда значение дуальной карты на линейной комбинации по f: b.toDual(Finsupp.linearCombination R b f)(b_i) = f_i для каждого i.
LaTeX
$$$ b.toDual (Finsupp.linearCombination R b f) (b i) = f i. $$$
Lean4
@[simp]
theorem toDual_linearCombination_left (f : ι →₀ R) (i : ι) : b.toDual (Finsupp.linearCombination R b f) (b i) = f i :=
by
rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, LinearMap.sum_apply]
simp_rw [LinearMap.map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq',
Finsupp.if_mem_support]
