add_pow_prime_eq — Mathlib

English

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

Русский

Пусть R — полукольцо и p простое. Если x и y коммутируют, то\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

protected theorem add_pow_prime_eq (h : Commute x y) :
    (x + y) ^ p = x ^ p + y ^ p + p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p) := by
  simpa using h.add_pow_prime_pow_eq hp 1

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