normal_self

Mathlib.FieldTheory.Normal.Defs

URI: https://scilib.ai/kg/mathlib#normal_self

← MathLib Explorer

English

The base field F is normal over itself: Normal F F.

Русский

Базовое поле F нормально над самим собой: Normal F F.

LaTeX

$$$\mathrm{Normal} F F$$$

Lean4

instance normal_self : Normal F F
    where
  isAlgebraic := fun _ => isIntegral_algebraMap.isAlgebraic
  splits' := fun x => (minpoly.eq_X_sub_C' x).symm ▸ splits_X_sub_C _

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

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

Разделы

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

Аффилиация

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