isIntegral'

Mathlib.FieldTheory.PurelyInseparable.Basic

URI: https://scilib.ai/kg/mathlib#IsPurelyInseparable.isIntegral'

English

In an IsPurelyInseparable extension, every element is integral over the base field.

Русский

В расширении IsPurelyInseparable каждый элемент целочислен над базовым полем.

LaTeX

$$$\forall x\in E,\ IsIntegral F x$$$

Lean4

theorem isIntegral' [IsPurelyInseparable F E] (x : E) : IsIntegral F x :=
  Algebra.IsIntegral.isIntegral _

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

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

Разделы

Аффилиация

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