chore: delete unused letI and nolint (#6523)

leanprover-community · Aug 11, 2023 · 5b3ada4 · 5b3ada4
1 parent ecc61a3
commit 5b3ada4
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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