perfectField — Mathlib

English

If E is a perfect field, then the relative perfect closure of E is a perfect field.

Русский

Если E — идеальное поле, то относительное идеальное замыкание E — тоже идеальное поле.

LaTeX

$$PerfectField(F,E) ⇒ PerfectField(perfectClosure(F,E))$$

Lean4

/-- If `E` is a perfect field, then the (relative) perfect closure
`perfectClosure F E` is perfect. -/
instance perfectField [PerfectField E] : PerfectField (perfectClosure F E) :=
  PerfectRing.toPerfectField _ (ringExpChar E)

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