sum_cramer — Mathlib

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

Похожие утверждения