add_pow_prime_eq — Mathlib

English

Let x,y commute in a semiring R and p be prime. Then\n (x + y)^p = x^p + y^p + p · ∑_{k=1}^{p-1} x^k y^{p-k} · (C(p,k)/p).

Русский

Пусть x,y коммутируют в полукольце R, p — простое. Тогда\n (x + y)^p = x^p + y^p + p · ∑_{k=1}^{p-1} x^k y^{p-k} · (C(p,k)/p).

LaTeX

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

Lean4

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

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