splits_zmod_X_pow_sub_X — Mathlib

English

Over the base field ZMod p, the polynomial X^p - X splits completely.

Русский

Над полем ZMod p многочлен X^p - X распадается на линейные множители.

LaTeX

$$Splits (RingHom.id (ZMod p)) (X^p - X)$$

Lean4

theorem splits_zmod_X_pow_sub_X : Splits (RingHom.id (ZMod p)) (X ^ p - X) :=
  by
  have hp : 1 < p := h_prime.out.one_lt
  have h1 : roots (X ^ p - X : (ZMod p)[X]) = Finset.univ.val :=
    by
    convert FiniteField.roots_X_pow_card_sub_X (ZMod p)
    exact (ZMod.card p).symm
  have h2 := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp
  cases p; cases hp
  rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]

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