add_pow_eq_mul_pow_add_pow_div_char

English

Let x,y commute in R with ExpChar R p. Then for any n,\n (x + y)^n = (x + y)^{n mod p} · (x^p + y^p)^{⌊n/p⌋}.

Русский

Пусть x,y коммутируют в R и ExpChar R p. Тогда для любого n:\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_eq_mul_pow_add_pow_div_char : (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p) :=
  add_pow_eq_mul_pow_add_pow_div_expChar ..

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