roots_X_pow_char_sub_X_bot — Mathlib

English

In the prime subfield, the polynomial X^p − X has all its roots; equivalently, its roots are all elements of the bottom subfield.

Русский

В простом подполе многочлен X^p − X имеет все свои корни; корни лежат в нижнем подполе.

LaTeX

$$$\\\\text{Let } F: \\\\text{field}, p \\\\text{ prime}. \\\\ (X^p - X) \\\\text{in } (⊥:Subtitle F)[X] \\\\text{has all roots }=\\\\ Finset.univ.$$

Lean4

theorem roots_X_pow_char_sub_X_bot :
    letI := Subfield.fintypeBot F p
    (X ^ p - X : (⊥ : Subfield F)[X]).roots = Finset.univ.val :=
  by
  let _ := Subfield.fintypeBot F p
  conv_lhs => rw [← card_bot F p, ← Fintype.card_eq_nat_card]
  exact FiniteField.roots_X_pow_card_sub_X _

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