exists_add_pow_prime_pow_eq — Mathlib

English

Let R be a semiring, p prime, and x,y commute in R. Then for every n there exists r ∈ R such that\n (x + y)^{p^n} = x^{p^n} + y^{p^n} + p · r.

Русский

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

LaTeX

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

Lean4

protected theorem exists_add_pow_prime_pow_eq (h : Commute x y) (n : ℕ) :
    ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + p * r :=
  ⟨_, h.add_pow_prime_pow_eq hp n⟩

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