self_of_isSepClosed

Mathlib.FieldTheory.IsSepClosed

URI: https://scilib.ai/kg/mathlib#IsSepClosure.self_of_isSepClosed

← MathLib Explorer

English

A separably closed field is equal to its separable closure.

Русский

Разделяемо замкнутое поле равно своему сепарабельному замыканию.

LaTeX

$$IsSepClosure k k$$

Lean4

/-- A separably closed field is its separable closure. -/
instance self_of_isSepClosed [IsSepClosed k] : IsSepClosure k k :=
  ⟨by assumption, Algebra.isSeparable_self k⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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