of_isAlgClosed

Mathlib.FieldTheory.IsSepClosed

URI: https://scilib.ai/kg/mathlib#IsSepClosed.of_isAlgClosed

← MathLib Explorer

English

An algebraically closed field is separably closed.

Русский

Алгебраически замкнутое поле является разделимо замкнутым.

LaTeX

$$$ \text{IsAlgClosed}(k) \Rightarrow \text{IsSepClosed}(k) $$$

Lean4

/-- An algebraically closed field is also separably closed. -/
instance of_isAlgClosed [IsAlgClosed k] : IsSepClosed k :=
  ⟨fun p _ ↦ IsAlgClosed.splits p⟩

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

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

Разделы

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

Аффилиация

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