add_pow_prime_pow_eq — Mathlib

English

Let R be a semiring and p prime. If x and y commute in R, then\n (x + y)^{p^n} = x^{p^n} + y^{p^n} + p · ∑... (as in 5420).

Русский

Пусть R — полукольцо, p простое. Если x и y коммутируют, то\n (x + y)^{p^n} = x^{p^n} + y^{p^n} + p · сумма(...), как в 5420.

LaTeX

$$$(x+y)^{p^n} = x^{p^n} + y^{p^n} + p \\sum_{k=1}^{p^n-1} x^{k} y^{p^n-k} \\dfrac{\\binom{p^n}{k}}{p}$$$

Lean4

theorem add_pow_prime_pow_eq :
    (x + y) ^ p ^ n =
      x ^ p ^ n + y ^ p ^ n + p * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) :=
  (Commute.all x y).add_pow_prime_pow_eq hp n

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