isSepClosed

Mathlib.FieldTheory.SeparableClosure

URI: https://scilib.ai/kg/mathlib#SeparableClosure.isSepClosed

English

For any field F, the separable closure of F is separably closed.

Русский

Для поля F сепарабельное замыкание F является сепарабельно-закрытым полем.

LaTeX

$$$\\mathrm{IsSepClosed}(\\mathrm{SeparableClosure}(F))$$$

Lean4

instance isSepClosed : IsSepClosed (SeparableClosure F) :=
  (inferInstanceAs (IsSepClosure F (SeparableClosure F))).sep_closed

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

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

Разделы

Аффилиация

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