exists_add_pow_prime_eq — Mathlib

English

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

Русский

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

protected theorem exists_add_pow_prime_eq (h : Commute x y) : ∃ r, (x + y) ^ p = x ^ p + y ^ p + p * r :=
  ⟨_, h.add_pow_prime_eq hp⟩

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