isIntegral

Mathlib.FieldTheory.Normal.Defs

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

English

If K is normal over F, then every element x ∈ K is integral over F.

Русский

Если K нормально над F, то каждый элемент x ∈ K является интегралом над F.

LaTeX

$$$\mathrm{Normal} F K \Rightarrow \forall x \in K, \ IsIntegral F x$$$

Lean4

theorem isIntegral (_ : Normal F K) (x : K) : IsIntegral F x :=
  Algebra.IsIntegral.isIntegral x

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

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

Разделы

Аффилиация

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