English
For integers x,y and natural n, x^{2^n} − y^{2^n} factors as (∏_{i=0}^{n-1} (x^{2^i} + y^{2^i}))(x − y).
Русский
Для целых x,y и натурального n выражение x^{2^n} − y^{2^n} раскладывается как произведение (∏_{i=0}^{n-1} (x^{2^i} + y^{2^i})) и (x − y).
LaTeX
$$$x^{2^n} - y^{2^n} = \left(\prod_{i=0}^{n-1} (x^{2^i} + y^{2^i})\right)(x-y).$$$
Lean4
theorem pow_two_pow_sub_pow_two_pow [CommRing R] {x y : R} (n : ℕ) :
x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ Finset.range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y) := by
induction n with
| zero => simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]
| succ d
hd =>
suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
rw [Nat.succ_eq_add_one]
ring
