isPurelyInseparable_bot

Mathlib.FieldTheory.PurelyInseparable.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.isPurelyInseparable_bot

English

The bottom intermediate field of E/F is purely inseparable over F.

Русский

Нижнее промежуточное поле E/F является чисто бесприводимым над F.

LaTeX

$$$\text{IsPurelyInseparable}(F, \perp)$$$

Lean4

instance isPurelyInseparable_bot : IsPurelyInseparable F (⊥ : IntermediateField F E) :=
  (botEquiv F E).symm.isPurelyInseparable

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

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

Разделы

Аффилиация

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