English
If K is a field, p is a natural number, K has ExpChar p and PerfectRing K p, then there exists a PerfectField structure on K.
Русский
Если K — поле, p — натуральное, характер K равен p и K явл. совершенным кольцом относительно p, то на K можно надстроить структуру совершенного поля.
LaTeX
$$$ \exists \text{PerfectField } K \text{ given } [Field K] [ExpChar K p] [PerfectRing K p]. $$$
Lean4
theorem toPerfectField (K : Type*) (p : ℕ) [Field K] [ExpChar K p] [PerfectRing K p] : PerfectField K :=
by
obtain hp | ⟨hp⟩ := ‹ExpChar K p›
· exact ⟨Irreducible.separable⟩
refine PerfectField.mk fun hf ↦ ?_
rcases separable_or p hf with h | ⟨-, g, -, rfl⟩
· assumption
· exfalso; revert hf; haveI := Fact.mk hp; simp
