integral

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#IsGalois.integral

English

If E is IsGalois over F, then any x ∈ E is integral over F.

Русский

Если E является Галуа-расширением над F, то любой элемент x ∈ E интегрален над F.

LaTeX

$$$\\text{IsGalois } F E \\Rightarrow \\forall x \\in E,\\ IsIntegral F x$$$

Lean4

theorem integral [IsGalois F E] (x : E) : IsIntegral F x :=
  to_normal.isIntegral x

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

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

Разделы

Аффилиация

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