dickson_two_zero — Mathlib

English

For any ring R and any n, the 2-nd Dickson polynomial with a = 0 and k = 2 is X^n.

Русский

Для любого кольца R и любого n полином Диксона №2 при a = 0 и k = 2 равен X^n.

LaTeX

$$dickson\, 2\, 0\, n = X^n$$

Lean4

@[simp]
theorem dickson_two_zero : ∀ n : ℕ, dickson 2 (0 : R) n = X ^ n
  | 0 => by
    simp only [dickson_zero, pow_zero]
    norm_num
  | 1 => by simp only [dickson_one, pow_one]
  | n + 2 => by
    simp only [dickson_add_two, C_0, zero_mul, sub_zero]
    rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]

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