From 815df64843de99ebd4d171d3c95da0dc43f27bf6 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 7 Dec 2024 12:13:52 +0100 Subject: [PATCH] fix depration --- FormalBook/Chapter_06.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean index 20acb7c..f33f254 100644 --- 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} :=