sub_pow_eq_mul_pow_sub_pow_div_char_of_commute

English

Let x and y commute in a ring R of characteristic p. Then for any natural n, (x − y)^n = (x − y)^{n mod p} · (x^p − y^p)^{n/p}.

Русский

Пусть x и y коммутируют в кольце R характеристикой p. Тогда для любого натурального 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 sub_pow_eq_mul_pow_sub_pow_div_char_of_commute (h : Commute x y) :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p) :=
  sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute _ _ h

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