From 17dcb4e0c032b79afaa4f404b04e0d84061bd018 Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Fri, 11 Aug 2023 14:14:11 +0000 Subject: [PATCH] chore: delete unused letI and nolint (#6523) --- Mathlib/FieldTheory/IsAlgClosed/Classification.lean | 3 --- 1 file changed, 3 deletions(-) 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