add_pow_expChar_pow_of_commute — Mathlib

English

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

Русский

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

LaTeX

$$$(x+y)^{p^n} = x^{p^n} + y^{p^n}$$$

Lean4

theorem add_pow_expChar_pow_of_commute (h : Commute x y) : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n :=
  by
  obtain _ | hprime := hR
  · simp only [one_pow, pow_one]
  · let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
    simp [hr]

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