From 07a9af9a782e5c813f96c5a6ee78eb38c6d623fb Mon Sep 17 00:00:00 2001 From: Jz Pan Date: Fri, 19 Jan 2024 15:41:37 +0000 Subject: [PATCH] feat(FieldTheory/IsAlgClosed/Basic): add `IsAlgClosed.perfectField` instance (#9710) Co-authored-by: Junyan Xu --- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 5585ec8d6183c..53ba5e7b2fa37 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -283,6 +283,10 @@ noncomputable instance (priority := 100) perfectRing (p : ℕ) [Fact p.Prime] [C PerfectRing.ofSurjective k p fun _ => IsAlgClosed.exists_pow_nat_eq _ <| NeZero.pos p #align is_alg_closed.perfect_ring IsAlgClosed.perfectRing +noncomputable instance (priority := 100) perfectField [IsAlgClosed k] : PerfectField k := by + obtain _ | ⟨p, _, _⟩ := CharP.exists' k + exacts [.ofCharZero k, PerfectRing.toPerfectField k p] + /-- Algebraically closed fields are infinite since `Xⁿ⁺¹ - 1` is separable when `#K = n` -/ instance (priority := 500) {K : Type*} [Field K] [IsAlgClosed K] : Infinite K := by apply Infinite.of_not_fintype