exists_add_pow_prime_eq — Mathlib

English

Let R be a semiring and p prime. If x,y commute in R, then there exists r ∈ R with\n (x + y)^p = x^p + y^p + p · r.

Русский

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

LaTeX

$$$\\exists r \\in R:\\ (x+y)^p = x^p + y^p + p \\cdot r$$$

Lean4

theorem exists_add_pow_prime_eq : ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r :=
  (Commute.all x y).exists_add_pow_prime_eq hp

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