instPerfectField — Mathlib

English

PerfectClosure(K,p) is a PerfectField; i.e., it is a field with Frobenius bijective and related perfectness properties.

Русский

PerfectClosure(K,p) является PerfectField; поле с биективным Фробениусом и связанными свойствами совершенности.

LaTeX

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

Lean4

instance instPerfectField : PerfectField (PerfectClosure K p) :=
  PerfectRing.toPerfectField _ p

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