English
Linearity of cramer over sums: the sum of cramer A (f x) over x in s equals cramer A (sum over x in s f x).
Русский
Линейность отображения cramer над суммами: \\sum_{x∈s} cramer A (f x) = cramer A (\\sum_{x∈s} f x).
LaTeX
$$$$\\sum_{x \\in s} cramer A (f x) = cramer A\\bigl(\\sum_{x \\in s} f x\\bigr).$$$$
Lean4
/-- Use linearity of `cramer` to take it out of a summation. -/
theorem sum_cramer {β} (s : Finset β) (f : β → n → α) : (∑ x ∈ s, cramer A (f x)) = cramer A (∑ x ∈ s, f x) :=
(map_sum (cramer A) ..).symm