dickson_one_one_charP — Mathlib

English

For a natural prime p and a ring R of characteristic p, D_1 1 p = X^p (i.e., the p-th Dickson polynomial equals X^p).

Русский

Для простого числа p и кольца R характеристика p, D_1 1 p = X^p.

LaTeX

$$dickson\, 1\, (1 : R)\, p = X^p$$

Lean4

theorem dickson_one_one_charP (p : ℕ) [Fact p.Prime] [CharP R p] : dickson 1 (1 : R) p = X ^ p :=
  by
  have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by simp only [ZMod.castHom_apply, ZMod.cast_one']
  rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow, map_X]

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