fix depration

mo271 · Dec 7, 2024 · 815df64 · 815df64
1 parent addaa06
commit 815df64
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean
@@ -189,8 +189,8 @@ theorem wedderburn (h: Fintype R): IsField R := by
   have finclassa: ∀ (A : ConjClasses Rˣ), Fintype ↑(ConjClasses.carrier A) :=
     fun _ ↦ ConjClasses.instFintypeElemCarrier
 
-  have : ∀ (A :  ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out' A}) :=
-    fun _ ↦ setFintype (Set.centralizer {Quotient.out' _})
+  have : ∀ (A :  ConjClasses Rˣ), Fintype ↑(Set.centralizer {Quotient.out A}) :=
+    fun _ ↦ setFintype (Set.centralizer {Quotient.out _})
 
   letI fintypea : ∀ (A :  ConjClasses Rˣ), Fintype ↑{A |
       have := finclassa A; Fintype.card ↑(ConjClasses.carrier A) > 1} :=