coeff_sum — Mathlib

English

For any finite set s and functions x: α → HahnSeries Γ R, the coefficient at g of the sum over i in s equals the sum of the coefficients: (sum_{i∈s} x_i).coeff g = sum_{i∈s} (x_i).coeff g.

Русский

Пусть s конечно; тогда коэффициент при g от суммы по i∈s равен сумме коэффициентов: (∑_{i∈s} x_i).coeff(g) = ∑_{i∈s} x_i .coeff(g).

LaTeX

$$$$ (\sum_{i \in s} x_i).coeff(g) = \sum_{i \in s} (x_i).coeff(g). $$$$

Lean4

@[simp]
theorem coeff_sum {s : Finset α} {x : α → HahnSeries Γ R} (g : Γ) : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g :=
  cons_induction rfl (fun i s his hsum => by rw [sum_cons, sum_cons, coeff_add, hsum]) s

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