exists_add_pow_prime_pow_eq — Mathlib

English

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

Русский

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

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

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