instField

Mathlib.FieldTheory.PerfectClosure

URI: https://scilib.ai/kg/mathlib#PerfectClosure.instField

← MathLib Explorer

English

PerfectClosure(K,p) carries a field structure compatible with the base field K.

Русский

PerfectClosure(K,p) имеет структуру поля, совместимую с базовым полем K.

LaTeX

$$$\mathrm{Field}(\mathrm{PerfectClosure}(K,p)).$$$

Lean4

instance instField : Field (PerfectClosure K p) :=
  { (inferInstance : DivisionRing (PerfectClosure K p)), (inferInstance : CommRing (PerfectClosure K p)) with }

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

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

Разделы

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

Аффилиация

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