diff --git a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
index 71c302cf44bdd..3f1f3fc45759e 100644
--- a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
+++ b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean
@@ -207,13 +207,10 @@ private theorem ringEquivOfCardinalEqOfCharP (p : ℕ) [Fact p.Prime] [CharP K p
 
 /-- Two uncountable algebraically closed fields are isomorphic
 if they have the same cardinality and the same characteristic. -/
-@[nolint defLemma]
 theorem ringEquivOfCardinalEqOfCharEq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < #K)
     (hKL : #K = #L) : Nonempty (K ≃+* L) := by
   rcases CharP.char_is_prime_or_zero K p with (hp | hp)
   · haveI : Fact p.Prime := ⟨hp⟩
-    letI : Algebra (ZMod p) K := ZMod.algebra _ _
-    letI : Algebra (ZMod p) L := ZMod.algebra _ _
     exact ringEquivOfCardinalEqOfCharP p hK hKL
   · simp only [hp] at *
     letI : CharZero K := CharP.charP_to_charZero K