English
For x,y ∈ R with x y = 1, the polynomial dickson 1 1 n evaluated at x + y yields x^n + y^n for all n, and this relation can be checked by induction on n.
Русский
Если x,y ∈ R и x y = 1, то dickson 1 1 n, вычисленный в x + y, даёт x^n + y^n для всего n; доказательство идёт по индукции по n.
LaTeX
$$∀ n, (dickson 1 (1 : R) n).eval (x + y) = x^n + y^n$$
Lean4
theorem dickson_one_one_eval_add_inv (x y : R) (h : x * y = 1) : ∀ n, (dickson 1 (1 : R) n).eval (x + y) = x ^ n + y ^ n
| 0 => by simp only [pow_zero, dickson_zero]; norm_num
| 1 => by simp only [eval_X, dickson_one, pow_one]
| n + 2 =>
by
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two, C_1, eval_one]
conv_lhs => simp only [pow_succ', add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
ring
