splits_X_pow_card_sub_X

Mathlib.FieldTheory.Finite.GaloisField

URI: https://scilib.ai/kg/mathlib#FiniteField.splits_X_pow_card_sub_X

← MathLib Explorer

English

Over 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 _root_.FiniteField.splits_X_pow_card_sub_X : Splits (algebraMap (ZMod p) K) (X ^ Fintype.card K - X) :=
  (FiniteField.isSplittingField_sub K (ZMod p)).splits

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru