perfectField — Mathlib

English

For a prime p and an algebraically closed field k, the ring k has the structure of a PerfectRing k p.

Русский

При простом p и алгебраически замкнутом поле k кольцо k имеет структуру PerfectRing k p.

LaTeX

$$$\forall (k) [\mathrm{Field\;k}] [\mathrm{Fact}\;\mathrm{p.Prime}] [\mathrm{CharP}\;k\;p] [IsAlgClosed k],\; PerfectRing k p$$$

Lean4

noncomputable instance (priority := 100) perfectField [IsAlgClosed k] : PerfectField k :=
  by
  obtain _ | ⟨p, _, _⟩ := CharP.exists' k
  exacts [.ofCharZero, PerfectRing.toPerfectField k p]

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