multiset_sum_pow_char_pow — Mathlib

English

In a commutative semiring with CharP p, s.sum^{p^n} = sum (x^{p^n}) over s.

Русский

В коммутативном полусере с CharP p, сумма мультисета возведённого в p^n равна сумме по элементам возведённых в p^n.

LaTeX

$$$ s.sum^{p^n} = \sum (x^{p^n}) $ over s$$

Lean4

theorem multiset_sum_pow_char_pow (s : Multiset R) : s.sum ^ p ^ n = (s.map (· ^ p ^ n : R → R)).sum :=
  map_multiset_sum (iterateFrobenius R p n) _

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