add_pow_char_of_commute — Mathlib

English

Let R be a semiring and p prime with ExpChar R p and CharP R p. If x,y commute, then\n (x + y)^n = (x + y)^{n mod p} · (x^p + y^p)^{n/p}.

Русский

Пусть R — полукольцо, p простое, ExpChar R p и CharP R p. Если x и y коммутируют, то\n (x + y)^n = (x + y)^{n mod p} · (x^p + y^p)^{n/p}.

LaTeX

$$$(x+y)^n = (x+y)^{n \\bmod p} \\cdot (x^p + y^p)^{\\left\\lfloor n/p \\right\\rfloor}$$$

Lean4

theorem add_pow_char_of_commute (h : Commute x y) : (x + y) ^ p = x ^ p + y ^ p :=
  add_pow_expChar_of_commute _ h

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