splits

Mathlib.FieldTheory.Normal.Defs

URI: https://scilib.ai/kg/mathlib#Normal.splits

English

For any x ∈ K, the minimal polynomial of x over F splits over K.

Русский

Для любого x ∈ K минимальный многочлен над F раскладывается в K.

LaTeX

$$$\mathrm{Normal} F K \Rightarrow \forall x \in K, \mathrm{Splits} (\mathrm{algebraMap} F K) (\minpoly F x)$$$

Lean4

theorem splits (_ : Normal F K) (x : K) : Splits (algebraMap F K) (minpoly F x) :=
  Normal.splits' x

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

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

Разделы

Аффилиация

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