sum_pow_mem_span_pow — Mathlib

English

For Finset s, function f: ι → α and n ∈ ℕ, (sum i∈s f(i))^(|s| n + 1) lies in the span of { f(i)^(n+1) | i ∈ s }.

Русский

Для конечного множества s и функции f: ι → α, сумма ∑ f(i) в степени (|s| n + 1) лежит в span{ f(i)^(n+1) | i ∈ s }.

LaTeX

$$$\\Big(\\sum_{i \\in s} f(i)\\Big)^{|s| \\cdot n + 1} \\in \\operatorname{span}\\{ f(i)^{n+1} \\mid i \\in s \\}$$$

Lean4

theorem sum_pow_mem_span_pow {ι} (s : Finset ι) (f : ι → α) (n : ℕ) :
    (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' s) := by
  classical
    simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map, Finset.coe_image,
    Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n

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