splits_bot — Mathlib

English

The polynomial X^p − X splits completely over the prime subfield ⊥.

Русский

Многочлен X^p − X раскладывается полностью над простым подполем ⊥.

LaTeX

$$$\\\\text{Splits}(\\\\text{RingHom.id}((⊥: Subfield F)), X^p - X)$$$$

Lean4

theorem splits_bot : Splits (RingHom.id (⊥ : Subfield F)) (X ^ p - X) :=
  by
  let _ := Subfield.fintypeBot F p
  rw [splits_iff_card_roots, roots_X_pow_char_sub_X_bot, ← Finset.card_def, Finset.card_univ,
    FiniteField.X_pow_card_sub_X_natDegree_eq _ (Fact.out (p := p.Prime)).one_lt, Fintype.card_eq_nat_card,
    card_bot F p]

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