list_sum_pow_char — Mathlib

English

For a list l in a commutative semiring of characteristic p, (sum l)^p = sum (l_i^p).

Русский

Для списка элементов в коммутативном полусколье характеристикой p справедливо (сумма)^p = сумма (элементов)^p.

LaTeX

$$$\left(\sum_{i} f(i)\right)^p = \sum_{i} f(i)^p$$$

Lean4

theorem list_sum_pow_char (l : List R) : l.sum ^ p = (l.map (· ^ p : R → R)).sum :=
  map_list_sum (frobenius R p) _

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