English
For a finite set s and function f, the sum of cramer A (f j x) over x ∈ s equals cramer A (sum over s f j x) for each coordinate j.
Русский
Для конечного множества s и функции f сумма cramer A (f j x) по x ∈ s равна cramer A (sum over s f j x) по координате j.
LaTeX
$$$$\\sum_{x \\in s} \\mathrm{cramer} A (f\\cdot x)_i = \\mathrm{cramer} A\\bigl(\\sum_{x\\in s} f\\, x\\bigr)_i.$$$$
Lean4
/-- Use linearity of `cramer` and vector evaluation to take `cramer A _ i` out of a summation. -/
theorem sum_cramer_apply {β} (s : Finset β) (f : n → β → α) (i : n) :
(∑ x ∈ s, cramer A (fun j => f j x) i) = cramer A (fun j : n => ∑ x ∈ s, f j x) i :=
calc
(∑ x ∈ s, cramer A (fun j => f j x) i) = (∑ x ∈ s, cramer A fun j => f j x) i := (Finset.sum_apply i s _).symm
_ = cramer A (fun j : n => ∑ x ∈ s, f j x) i :=
by
rw [sum_cramer, cramer_apply, cramer_apply]
simp only [updateCol]
congr with j
congr
apply Finset.sum_apply
