feat(FieldTheory/IsAlgClosed/Basic): add IsAlgClosed.perfectField i…

…nstance (#9710)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

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