Source indexedlemma · leanprover/lean4:v4.32.0

Finset.pow_sum_comm

Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:760 to 770

Mathematical statement

Exact Lean statement

lemma Finset.pow_sum_comm {ι R : Type*} [Semiring R] {s : Finset ι} {f : ι → R}
    (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i * f j = 0) {n : ℕ} (hn : 1 ≤ n) :
    (∑ i ∈ s, f i) ^ n = ∑ i ∈ s, f i ^ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Finset.pow_sum_comm {ι R : Type*} [Semiring R] {s : Finset ι} {f : ι → R}    (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i * f j = 0) {n : ℕ} (hn : 1 ≤ n) :    (∑ i ∈ s, f i) ^ n = ∑ i ∈ s, f i ^ n := by  induction n, hn using Nat.le_induction with  | base => simp  | succ n hn ih =>    simp_rw [pow_succ, ih, sum_mul, mul_sum]    congr! 1 with x mx    refine Finset.sum_eq_single _ (fun y my hn ↦ ?_) (fun _ ↦ by contradiction)    rw [← Nat.sub_one_add_one (show n ≠ 0 by lia), pow_succ, mul_assoc, hf _ mx _ my hn.symm,      mul_zero]