English
Let R be a semiring and p a prime. If x and y commute in R, then for every n ≥ 0,\n(x + y)^{p^n} = x^{p^n} + y^{p^n} + p · ∑_{k=1}^{p^n-1} x^k y^{p^n-k} · (C(p^n,k)/p),\nwhere C(p^n,k) is the binomial coefficient and the factors are interpreted in R.
Русский
Пусть R — полукольцо и p — простое число. Если элементы x и y коммутируют в R, то для любого n ≥ 0 выполняется:\n(x + y)^{p^n} = x^{p^n} + y^{p^n} + p · ∑_{k=1}^{p^n-1} x^k y^{p^n-k} · (C(p^n,k)/p),\ где C(p^n,k) — биномиальный коэффициент, а множители трактуются в R.
LaTeX
$$$(x+y)^{p^n} = x^{p^n} + y^{p^n} + p \\sum_{k=1}^{p^n-1} x^{k} y^{p^n-k} \\dfrac{\\binom{p^n}{k}}{p}$$$
Lean4
protected theorem add_pow_prime_pow_eq (h : Commute x y) (n : ℕ) :
(x + y) ^ p ^ n =
x ^ p ^ n + y ^ p ^ n + p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) :=
by
trans x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (p ^ n).choose k
·
simp_rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc, Icc_eq_cons_Ico (zero_le _), Finset.sum_cons,
Ico_eq_cons_Ioo (pow_pos hp.pos _), Finset.sum_cons, tsub_self, tsub_zero, pow_zero, Nat.choose_zero_right,
Nat.choose_self, Nat.cast_one, mul_one, one_mul, ← add_assoc]
· congr 1
simp_rw [Finset.mul_sum, Nat.cast_comm, mul_assoc _ _ (p : R), ← Nat.cast_mul]
refine Finset.sum_congr rfl fun i hi => ?_
rw [mem_Ioo] at hi
rw [Nat.div_mul_cancel (hp.dvd_choose_pow hi.1.ne' hi.2.ne)]
