English
Let R be a semiring and M an R-module. For index sets α, β and maps A: α → M, B: β → α →₀ R, and f: β →₀ R, the outer linear combination distributes over the inner one: linearCombination R A (linearCombination R B f) = linearCombination R (λ b, linearCombination R A (B b)) f.
Русский
Пусть R — полугруппа, M — модуль над R. Пусть A: α → M, B: β → α →₀ R и f: β →₀ R. Тогда внешняя линейная комбинация распределяется над внутренней: линейная комбинация R A (линейная комбинация R B f) равна линейной комбинации R по функции b ↦ линейная комбинация R A (B b) применённой к f.
LaTeX
$$$\\operatorname{linearCombination}_R(A,\\operatorname{linearCombination}_R(B,f)) = \\operatorname{linearCombination}_R\\bigl(\\lambda b. \\operatorname{linearCombination}_R(A, B b)\\bigr) f$$$
Lean4
theorem linearCombination_linearCombination {α β : Type*} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) :
linearCombination R A (linearCombination R B f) = linearCombination R (fun b => linearCombination R A (B b)) f := by
classical
simp only [linearCombination_apply]
induction f using induction_linear with
| zero => simp only [sum_zero_index]
| add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
| single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]
