isSplittingField_of_card_eq — Mathlib

English

If K is a finite field with cardinality p^n, then ZMod p is the base field and X^{p^n} - X has splitting field K.

Русский

Если K — конечное поле с кардинальностью p^n, то ZMod p — базовое поле, и X^{p^n} - X распадается в K.

LaTeX

$$IsSplittingField (ZMod p) K (X ^ p ^ n - X)$$

Lean4

theorem _root_.FiniteField.isSplittingField_of_card_eq (h : Fintype.card K = p ^ n) :
    IsSplittingField (ZMod p) K (X ^ p ^ n - X) :=
  h ▸ FiniteField.isSplittingField_sub K (ZMod p)

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