out

Mathlib.FieldTheory.Normal.Defs

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

English

From the previous characterization, derive the explicit normal_iff statement.

Русский

Из предыдущей характеристики следует явное утверждение normal_iff.

LaTeX

$$$\mathrm{Normal} F K \Rightarrow \forall x \in K, \; \text{(IsIntegral F x and Splits ...)}$$$

Lean4

theorem out : Normal F K → ∀ x : K, IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x) :=
  normal_iff.1

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

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

Разделы

Аффилиация

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