diff --git a/Book/Elements.lean b/Book/Elements.lean
index ea92e21..c3625a8 100644
--- a/Book/Elements.lean
+++ b/Book/Elements.lean
@@ -78,7 +78,8 @@ unter Inversenbildung“ — ist in Mathlib die Konstruktion
 `IntermediateField.adjoin.powerBasis`: Für ganzes $`a` baut sie
 aus den Potenzen $`1, a, …, a^{m-1}` eine Basis von `K⟮a⟯`, eine
 sogenannte _Potenzbasis_.  Wie bei der Gradformel bleibt für uns
-das Abzählen der Basis.
+das Abzählen der Basis — und wie dort holen wir den vollständigen
+Beweis am Ende des Kapitels nach.
 
 ```lean
 open IntermediateField
@@ -131,7 +132,9 @@ Genau dieses Argument — adjungiere die endlich vielen
 Koeffizienten des Minimalpolynoms, schließe auf Endlichkeit und
 klettere mit der Gradformel den Turm hinauf — steckt in Mathlib
 im Lemma `isIntegral_trans`.  Unser Beweis übersetzt die
-Rahmensätze des Skripts und zitiert für den Kern dieses Lemma:
+Rahmensätze des Skripts und zitiert für den Kern dieses Lemma;
+der letzte Abschnitt des Kapitels führt auch diesen Beweis
+Satz für Satz aus:
 
 ```lean
 theorem transitivitaet (K L M : Type*) [Field K] [Field L]
@@ -207,3 +210,483 @@ theorem algebraisch_quadrat {K L : Type*} [Field K]
     IsIntegral K (a ^ 2 + a) := by
   sorry
 ```
+
+# Der vollständige Beweis von Satz 3.5.4
+
+Oben haben wir die eigentliche Arbeit — die Potenzen bilden eine
+Basis von $`K(a)` — bei `IntermediateField.adjoin.powerBasis`
+eingekauft.  Jetzt führen wir den Skript-Beweis Satz für Satz
+selbst aus.  Er ist deutlich länger als der vollständige Beweis
+der Gradformel, denn das Skript zeigt hier wirklich etwas
+Substantielles: dass ein endlichdimensionaler Untervektorraum,
+der unter Multiplikation abgeschlossen ist, automatisch auch
+Inverse enthält.
+
+Die Hauptfigur ist der Untervektorraum aus dem Skript:
+
+> Betrachte deshalb den $`m`-dimensionalen Untervektorraum
+  $`V := \langle 1, a, a^2, …, a^{m-1} \rangle_K ⊆ K(a)`.
+
+```lean
+open Polynomial
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+
+-- Der Untervektorraum V = ⟨1, a, …, a^{m-1}⟩ des Skripts.
+noncomputable def potenzraum (K : Type*) {L : Type*}
+    [Field K] [Field L] [Algebra K L] (a : L) :
+    Submodule K L :=
+  Submodule.span K (Set.range
+    fun i : Fin (minpoly K a).natDegree => a ^ (i : ℕ))
+```
+
+Ein Argument benutzt das Skript zweimal — einmal für $`a`, später
+noch einmal für ein Element $`y ∈ V`:
+
+> Falls nicht, dann gäbe es eine Zahl $`m ∈ ℕ` und Elemente
+  $`λ_0, …, λ_m ∈ K`, die nicht alle gleich Null sind, sodass
+  $`0 = \sum_{i} λ_i \cdot a^i` ist.  Dann wäre $`a` aber eine
+  Nullstelle des Polynoms $`f(x) = \sum_i λ_i \cdot x^i ∈ K[x]`,
+  welches nicht das Nullpolynom ist.
+
+Wir formulieren es deshalb als eigenes Hilfslemma: Eine
+nichttriviale lineare Relation unter den Potenzen liefert ein
+Polynom.
+
+```lean
+theorem polynom_aus_relation {k : ℕ} (y : L) (μ : Fin k → K)
+    (hrel : ∑ i, μ i • y ^ (i : ℕ) = 0) (i₀ : Fin k)
+    (hμ : μ i₀ ≠ 0) :
+    ∃ g : K[X],
+      g ≠ 0 ∧ g.degree < (k : ℕ) ∧ aeval y g = 0 := by
+  -- Das Polynom g = ∑ μᵢ·xⁱ …
+  refine ⟨∑ i : Fin k, C (μ i) * X ^ (i : ℕ), ?_, ?_, ?_⟩
+  -- „… welches nicht das Nullpolynom ist“: sein i₀-ter
+  -- Koeffizient ist μᵢ₀ ≠ 0.
+  · intro h0
+    apply hμ
+    have hc := congrArg (fun g => coeff g (i₀ : ℕ)) h0
+    simpa [finsetSum_coeff, coeff_C_mul, coeff_X_pow,
+      Fin.val_inj] using hc
+  -- … hat Grad < k …
+  · refine lt_of_le_of_lt (degree_sum_le _ _) ?_
+    rw [Finset.sup_lt_iff
+      (by exact_mod_cast WithBot.bot_lt_coe k)]
+    intro i _
+    exact lt_of_le_of_lt (degree_C_mul_X_pow_le _ _)
+      (by exact_mod_cast i.isLt)
+  -- … und „y wäre eine Nullstelle des Polynoms“.
+  · rw [map_sum]
+    simp_rw [map_mul, aeval_C, map_pow, aeval_X,
+      ← Algebra.smul_def]
+    exact hrel
+```
+
+Damit folgt die lineare Unabhängigkeit wie im Skript:
+
+> Die Menge $`\{1, a, a^2, …, a^{m-1}\} ⊆ K(a)` ist linear
+  unabhängig über $`K`: Jede nicht-triviale Linearkombination
+  der Null lieferte nämlich ein Polynom vom Grad kleiner $`m`,
+  welches nicht das Nullpolynom ist und $`a` als Nullstelle
+  hat — im Widerspruch zur Minimalität des Grades des
+  Minimalpolynoms.
+
+Die „Minimalität des Grades“ heißt in Mathlib
+`minpoly.degree_le_of_ne_zero`.
+
+```lean
+theorem potenzen_unabhaengig {a : L} (ha : IsIntegral K a) :
+    LinearIndependent K
+      (fun i : Fin (minpoly K a).natDegree =>
+        a ^ (i : ℕ)) := by
+  rw [Fintype.linearIndependent_iff]
+  intro μ hrel i₀
+  by_contra hμ
+  -- „Jede nicht-triviale Linearkombination der Null
+  --  lieferte ein Polynom vom Grad kleiner m … mit a als
+  --  Nullstelle“
+  obtain ⟨g, hg0, hdeg, hroot⟩ :=
+    polynom_aus_relation a μ hrel i₀ hμ
+  -- „im Widerspruch zur Minimalität des Grades des
+  --  Minimalpolynoms.“
+  have hle := minpoly.degree_le_of_ne_zero K a hg0 hroot
+  rw [degree_eq_natDegree (minpoly.ne_zero ha)] at hle
+  exact absurd (hle.trans_lt hdeg) (lt_irrefl _)
+```
+
+Nun der erste Schritt des Skripts:
+
+> _Schritt 1: Abgeschlossenheit unter Multiplikation._ Weil
+  $`a` eine Nullstelle des Minimalpolynoms $`f` ist, gilt die
+  Gleichung $`a^m = -\sum_{i=0}^{m-1} λ_i \cdot a^i ∈ V`.
+  Durch wiederholte Anwendung dieser Gleichung folgt induktiv,
+  dass $`a^n ∈ V` ist, für alle Zahlen $`n ∈ ℕ`.  Jedes Produkt
+  von Elementen aus $`V` ist eine $`K`-Linearkombination von
+  Potenzen von $`a`, also gilt für alle $`v_1, v_2 ∈ V`, dass
+  $`v_1 \cdot v_2 ∈ V` ist.
+
+```lean
+-- „Weil a eine Nullstelle des Minimalpolynoms f ist, gilt
+--  die Gleichung a^m = -∑ λᵢ·aⁱ.“
+theorem hoechste_potenz {a : L} (ha : IsIntegral K a) :
+    a ^ (minpoly K a).natDegree =
+      -∑ i ∈ Finset.range (minpoly K a).natDegree,
+        (minpoly K a).coeff i • a ^ i := by
+  have h := minpoly.aeval K a
+  rw [aeval_eq_sum_range, Finset.sum_range_succ,
+    (minpoly.monic ha).coeff_natDegree, one_smul] at h
+  exact eq_neg_of_add_eq_zero_right h
+
+-- „Durch wiederholte Anwendung dieser Gleichung folgt
+--  induktiv, dass aⁿ ∈ V ist, für alle Zahlen n ∈ ℕ.“
+theorem potenz_mem {a : L} (ha : IsIntegral K a) (n : ℕ) :
+    a ^ n ∈ potenzraum K a := by
+  induction n using Nat.strong_induction_on with
+  | _ n IH =>
+    by_cases hn : n < (minpoly K a).natDegree
+    · exact Submodule.subset_span ⟨⟨n, hn⟩, rfl⟩
+    · rw [not_lt] at hn
+      have hm0 : 0 < (minpoly K a).natDegree :=
+        minpoly.natDegree_pos ha
+      have hsplit : a ^ n =
+          a ^ (n - (minpoly K a).natDegree)
+            * a ^ (minpoly K a).natDegree := by
+        rw [← pow_add]
+        congr 1
+        omega
+      rw [hsplit, hoechste_potenz ha, mul_neg,
+        Finset.mul_sum]
+      refine Submodule.neg_mem _
+        (Submodule.sum_mem _ fun i hi => ?_)
+      rw [mul_smul_comm, ← pow_add]
+      refine Submodule.smul_mem _ _ (IH _ ?_)
+      have := Finset.mem_range.mp hi
+      omega
+
+-- „Jedes Produkt von Elementen aus V ist eine
+--  K-Linearkombination von Potenzen von a, also gilt für
+--  alle v₁, v₂ ∈ V, dass v₁·v₂ ∈ V ist.“
+theorem produkt_mem {a : L} (ha : IsIntegral K a) {x y : L}
+    (hx : x ∈ potenzraum K a) (hy : y ∈ potenzraum K a) :
+    x * y ∈ potenzraum K a := by
+  induction hx, hy using Submodule.span_induction₂ with
+  | mem_mem u v hu hv =>
+    obtain ⟨i, rfl⟩ := hu
+    obtain ⟨j, rfl⟩ := hv
+    simpa [pow_add] using potenz_mem ha ((i : ℕ) + (j : ℕ))
+  | zero_left v hv => simp
+  | zero_right u hu => simp
+  | add_left u v w _ _ hw h1 h2 =>
+    rw [add_mul]
+    exact Submodule.add_mem _ h1 h2
+  | add_right u v w hu _ _ h1 h2 =>
+    rw [mul_add]
+    exact Submodule.add_mem _ h1 h2
+  | smul_left r u v _ _ h =>
+    rw [smul_mul_assoc]
+    exact Submodule.smul_mem _ _ h
+  | smul_right r u v _ _ h =>
+    rw [mul_smul_comm]
+    exact Submodule.smul_mem _ _ h
+```
+
+Das „Jedes Produkt … ist eine $`K`-Linearkombination“ erledigt
+`Submodule.span_induction₂`: Es genügt, die Behauptung für die
+erzeugenden Potenzen zu prüfen (der Fall `mem_mem`, dort ist
+$`a^i \cdot a^j = a^{i+j}`); Summen und Vielfache vererben sich.
+
+Der zweite Schritt ist das Herzstück:
+
+> _Schritt 2: Abgeschlossenheit unter Inversenbildung._ Es sei
+  $`y ∈ V` mit $`y ≠ 0` gegeben.  Weil $`V` abgeschlossen unter
+  der Multiplikation ist, liegen alle Potenzen
+  $`1, y, y^2, …, y^m` in $`V`.  Das sind $`m+1` Elemente in
+  einem Vektorraum der Dimension $`m`, also sind diese Elemente
+  linear abhängig über $`K`.  Insbesondere ist $`y` algebraisch
+  über $`K`.  Es sei $`g(x) = c_0 + c_1 x + ⋯ + x^n` das
+  Minimalpolynom von $`y` über $`K`.  Dann ist $`c_0 ≠ 0`:
+  Andernfalls könnte ich nämlich in $`g` einmal $`x`
+  ausklammern, also $`g = x \cdot h` schreiben.  Weil $`K(a)`
+  ein Körper und $`y ≠ 0` ist, folgte aus
+  $`0 = g(y) = y \cdot h(y)` schon $`h(y) = 0` — im Widerspruch
+  zur Minimalität des Grades von $`g`.  Aus der Gleichung
+  $`0 = g(y) = y \cdot (y^{n-1} + c_{n-1} y^{n-2} + ⋯ + c_1) + c_0`
+  folgt jetzt $`1/y = (y^{n-1} + ⋯ + c_1)/(-c_0) ∈ V`, denn der
+  Zähler ist eine $`K`-Linearkombination von Potenzen von $`y`,
+  liegt also in $`V`, und der Nenner $`-c_0` liegt in $`K`.
+
+Das Zählargument „$`m+1` Elemente in Dimension $`m`“ ist
+`LinearIndependent.fintype_card_le_finrank`; die Dimension von
+$`V` kennen wir aus der linearen Unabhängigkeit
+(`finrank_span_eq_card`).
+
+```lean
+theorem invers_mem {a : L} (ha : IsIntegral K a) {y : L}
+    (hy : y ∈ potenzraum K a) (hy0 : y ≠ 0) :
+    y⁻¹ ∈ potenzraum K a := by
+  -- „Weil V abgeschlossen unter der Multiplikation ist,
+  --  liegen alle Potenzen 1, y, y², … in V.“
+  have hyn : ∀ j : ℕ, y ^ j ∈ potenzraum K a := by
+    intro j
+    induction j with
+    | zero => simpa using potenz_mem ha 0
+    | succ j IH =>
+      rw [pow_succ]
+      exact produkt_mem ha IH hy
+  -- „Das sind m+1 Elemente in einem Vektorraum der
+  --  Dimension m, also sind diese Elemente linear abhängig
+  --  über K.“
+  have hfin : FiniteDimensional K (potenzraum K a) := by
+    unfold potenzraum
+    exact FiniteDimensional.span_of_finite K
+      (Set.finite_range _)
+  have hdim : Module.finrank K (potenzraum K a)
+      = (minpoly K a).natDegree := by
+    unfold potenzraum
+    rw [finrank_span_eq_card (potenzen_unabhaengig ha),
+      Fintype.card_fin]
+  have habh : ¬ LinearIndependent K
+      (fun i : Fin ((minpoly K a).natDegree + 1) =>
+        (⟨y ^ (i : ℕ), hyn i⟩ : potenzraum K a)) := by
+    intro h
+    have hcard := h.fintype_card_le_finrank
+    rw [Fintype.card_fin, hdim] at hcard
+    omega
+  -- „Insbesondere ist y algebraisch über K.“
+  rw [Fintype.not_linearIndependent_iff] at habh
+  obtain ⟨μ, hrel, i₀, hμ0⟩ := habh
+  have hrelL : ∑ i : Fin ((minpoly K a).natDegree + 1),
+      μ i • y ^ (i : ℕ) = 0 := by
+    simpa using congrArg
+      (Submodule.subtype (potenzraum K a)) hrel
+  obtain ⟨g, hg0, _, hgroot⟩ :=
+    polynom_aus_relation y μ hrelL i₀ hμ0
+  have hyint : IsIntegral K y :=
+    (IsAlgebraic.isIntegral ⟨g, hg0, hgroot⟩)
+  -- „Es sei g das Minimalpolynom von y über K.  Dann ist
+  --  c₀ ≠ 0: Andernfalls könnte ich nämlich in g einmal x
+  --  ausklammern, also g = x·h schreiben.  Weil K(a) ein
+  --  Körper und y ≠ 0 ist, folgte aus 0 = g(y) = y·h(y)
+  --  schon h(y) = 0 — im Widerspruch zur Minimalität des
+  --  Grades von g.“
+  have hc0 : (minpoly K y).coeff 0 ≠ 0 := by
+    intro h0
+    obtain ⟨h, hh⟩ := X_dvd_iff.mpr h0
+    have hhy : aeval y h = 0 := by
+      have haev := minpoly.aeval K y
+      rw [hh, map_mul, aeval_X] at haev
+      rcases mul_eq_zero.mp haev with h1 | h1
+      · exact absurd h1 hy0
+      · exact h1
+    have hhne : h ≠ 0 := by
+      rintro rfl
+      rw [mul_zero] at hh
+      exact minpoly.ne_zero hyint hh
+    have hle := minpoly.degree_le_of_ne_zero K y hhne hhy
+    rw [hh, mul_comm] at hle
+    exact absurd hle
+      (not_le.mpr (degree_lt_degree_mul_X hhne))
+  -- „Aus der Gleichung 0 = g(y) = y·(y^{n-1} + ⋯ + c₁) + c₀
+  --  folgt jetzt 1/y = (y^{n-1} + ⋯ + c₁)/(-c₀) ∈ V …“
+  have expand := minpoly.aeval K y
+  rw [aeval_eq_sum_range, Finset.sum_range_succ'] at expand
+  simp_rw [pow_succ, ← smul_mul_assoc, pow_zero] at expand
+  rw [← Finset.sum_mul] at expand
+  have hwy : (∑ i ∈ Finset.range (minpoly K y).natDegree,
+        (minpoly K y).coeff (i + 1) • y ^ i) * y
+      = -((minpoly K y).coeff 0 • 1) :=
+    eq_neg_of_add_eq_zero_left expand
+  have hone : y * ((-(minpoly K y).coeff 0)⁻¹ •
+      ∑ i ∈ Finset.range (minpoly K y).natDegree,
+        (minpoly K y).coeff (i + 1) • y ^ i) = 1 := by
+    rw [mul_smul_comm, mul_comm y, hwy, ← neg_smul,
+      smul_smul, inv_mul_cancel₀ (neg_ne_zero.mpr hc0),
+      one_smul]
+  rw [inv_eq_of_mul_eq_one_right hone]
+  -- „… denn der Zähler ist eine K-Linearkombination von
+  --  Potenzen von y, liegt also in V, und der Nenner -c₀
+  --  liegt in K.“
+  exact Submodule.smul_mem _ _
+    (Submodule.sum_mem _ fun i _ =>
+      Submodule.smul_mem _ _ (hyn i))
+```
+
+Bleibt der Zusammenbau:
+
+> Ich behaupte, dass $`V = K(a)` ist; damit ist dann
+  $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen.  Um die
+  Behauptung zu zeigen, genügt es zu zeigen, dass $`V` ein
+  Unterkörper von $`K(a)` ist.  Denn $`V` enthält $`K` und das
+  Element $`a`, und $`K(a)` ist per Definition der kleinste
+  Unterkörper, der $`K` und $`a` enthält.  Weil $`V` ein
+  Untervektorraum ist, ist $`V` abgeschlossen unter der
+  Addition.
+
+Das „Bündeln“ von $`V` mit den bewiesenen Abgeschlossenheiten zu
+einem Unterkörper ist in Lean das Ausfüllen der Strukturfelder
+von `Subalgebra` und `IntermediateField`; das „per Definition
+der kleinste Unterkörper“ ist `adjoin_simple_le_iff`.
+
+```lean
+theorem grad_element_vollstaendig {a : L}
+    (ha : IsIntegral K a) :
+    Module.finrank K K⟮a⟯ = (minpoly K a).natDegree := by
+  -- „… genügt es zu zeigen, dass V ein Unterkörper von K(a)
+  --  ist.“ — wir bündeln V zu einem Zwischenkörper F:
+  let A : Subalgebra K L :=
+    { carrier := potenzraum K a
+      mul_mem' := fun hx hy => produkt_mem ha hx hy
+      one_mem' := by simpa using potenz_mem ha 0
+      add_mem' := fun hx hy => Submodule.add_mem _ hx hy
+      zero_mem' := Submodule.zero_mem _
+      algebraMap_mem' := fun c => by
+        rw [Algebra.algebraMap_eq_smul_one]
+        exact Submodule.smul_mem _ _
+          (by simpa using potenz_mem ha 0) }
+  let F : IntermediateField K L :=
+    { A with
+      inv_mem' := fun x hx => by
+        by_cases hx0 : x = 0
+        · rw [hx0, inv_zero]
+          exact Submodule.zero_mem _
+        · exact invers_mem ha hx hx0 }
+  -- „Denn V enthält K und das Element a, und K(a) ist per
+  --  Definition der kleinste Unterkörper, der K und a
+  --  enthält.“
+  have haF : a ∈ F := by
+    show a ∈ potenzraum K a
+    simpa using potenz_mem ha 1
+  have oben : K⟮a⟯ ≤ F := adjoin_simple_le_iff.mpr haF
+  have unten : F ≤ K⟮a⟯ := by
+    intro x hx
+    have hVsub : potenzraum K a ≤
+        Subalgebra.toSubmodule K⟮a⟯.toSubalgebra := by
+      unfold potenzraum
+      rw [Submodule.span_le]
+      rintro _ ⟨i, rfl⟩
+      exact pow_mem (mem_adjoin_simple_self K a) _
+    exact hVsub hx
+  have hFK : F = K⟮a⟯ := le_antisymm unten oben
+  -- „… damit ist dann [K(a):K] = dim_K V = m und der Satz
+  --  ist bewiesen.“
+  rw [← hFK]
+  have h1 : Module.finrank K F
+      = Module.finrank K (potenzraum K a) :=
+    (Subalgebra.finrank_toSubmodule A).symm
+  rw [h1]
+  unfold potenzraum
+  rw [finrank_span_eq_card (potenzen_unabhaengig ha),
+    Fintype.card_fin]
+```
+
+# Der vollständige Beweis der Transitivität
+
+Zum Schluss der Skript-Beweis der Transitivität, ohne das Zitat
+von `isIntegral_trans` — die Kette $`K ⊆ Z ⊆ Z(m) ∋ m` wird
+wörtlich nachgebaut.  Das komplette Skript-Zitat steht oben;
+im Beweis stehen die Sätze wie immer als Kommentare.  Drei
+Übersetzungsentscheidungen vorweg:
+
+* Die Koeffizienten $`λ_i` des Minimalpolynoms liegen in $`L`;
+  das Skript liest sie stillschweigend als Elemente von $`M`.
+  In Lean geschieht das explizit über die Einbettung
+  `algebraMap L M`.  Die endliche Menge der Koeffizienten eines
+  Polynoms heißt `Polynomial.coeffs`.
+
+* „$`f` liegt in $`Z[x]`“ ist in Lean ein echter
+  Übersetzungsschritt: `Polynomial.toSubring` fasst ein Polynom,
+  dessen Koeffizienten in einem Teilring liegen, als Polynom
+  über diesem Teilring auf.
+
+* Das Skript zitiert zweimal Satz 3.6.5 (endlich erzeugt von
+  algebraischen Elementen ⟺ endlich ⟹ algebraisch); in Mathlib
+  sind das `IntermediateField.finiteDimensional_adjoin` und
+  `Algebra.IsAlgebraic.of_finite`.  Die Gradformel steckt in
+  `FiniteDimensional.trans`.
+
+```lean
+theorem transitivitaet_vollstaendig (K L M : Type*)
+    [Field K] [Field L] [Field M] [Algebra K L]
+    [Algebra L M] [Algebra K M] [IsScalarTower K L M]
+    [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic L M] :
+    Algebra.IsAlgebraic K M := by
+  constructor
+  -- „Es sei ein Element m ∈ M gegeben.“
+  intro x
+  -- „Wir wissen, dass m algebraisch über L ist; es sei f
+  --  das Minimalpolynom von m über L.“
+  have hxL : IsIntegral L x :=
+    (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
+  -- „Die Koeffizienten λᵢ liegen in L.“ — wir fassen sie
+  --  über die Einbettung L → M als Elemente von M auf.
+  set S : Set M :=
+    algebraMap L M '' ↑(minpoly L x).coeffs
+  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1})“
+  set Z : IntermediateField K M :=
+    IntermediateField.adjoin K S
+  -- „Die Erweiterung L/K ist algebraisch, also sind die
+  --  endlich vielen Elemente λ₀, …, λ_{n-1} allesamt
+  --  algebraisch über K.“
+  have hS : ∀ s ∈ S, IsIntegral K s := by
+    rintro _ ⟨c, _, rfl⟩
+    exact ((Algebra.IsAlgebraic.isAlgebraic
+        (R := K) c).isIntegral).map
+      (IsScalarTower.toAlgHom K L M)
+  have hSfin : S.Finite :=
+    Set.Finite.image _ (minpoly L x).coeffs.finite_toSet
+  have : Finite ↥S := hSfin.to_subtype
+  -- „Satz 3.6.5 sagt deshalb, dass [Z:K] < ∞ ist.“
+  have hZfin : FiniteDimensional K Z :=
+    IntermediateField.finiteDimensional_adjoin hS
+  -- „Weiter liegt das Polynom f in Z[x] und hat m als
+  --  Nullstelle.  Also ist m auch algebraisch über Z.“
+  have hxZ : IsIntegral Z x := by
+    have hco : (↑((minpoly L x).map (algebraMap L M)).coeffs
+        : Set M) ⊆ ↑Z.toSubalgebra.toSubring := by
+      intro c hc
+      obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hc
+      rw [coeff_map]
+      have hne : (minpoly L x).coeff n ≠ 0 := by
+        intro h0
+        rw [mem_support_iff, coeff_map, h0, map_zero] at hn
+        exact hn rfl
+      exact subset_adjoin K S
+        ⟨(minpoly L x).coeff n, coeff_mem_coeffs hne, rfl⟩
+    refine ⟨((minpoly L x).map (algebraMap L M)).toSubring
+      Z.toSubalgebra.toSubring hco, ?_, ?_⟩
+    · exact (monic_toSubring _ _ _).mpr
+        ((minpoly.monic hxL).map _)
+    · rw [show algebraMap Z M
+          = (Z.toSubalgebra.toSubring).subtype from rfl,
+        eval₂_eq_eval_map, map_toSubring, eval_map,
+        ← aeval_def, minpoly.aeval]
+  -- „… und Satz 3.5.4 liefert [Z(m):Z] < ∞.“
+  have hE : FiniteDimensional Z Z⟮x⟯ :=
+    IntermediateField.adjoin.finiteDimensional hxZ
+  -- „Mit der Gradformel folgt
+  --  [Z(m):K] = [Z(m):Z]·[Z:K] < ∞.“
+  have hZM : FiniteDimensional K (Z⟮x⟯.restrictScalars K) :=
+    FiniteDimensional.trans K Z Z⟮x⟯
+  -- „Wieder nach Satz 3.6.5 ist die Erweiterung Z(m)/K dann
+  --  algebraisch.“
+  have halg :
+      Algebra.IsAlgebraic K (Z⟮x⟯.restrictScalars K) :=
+    Algebra.IsAlgebraic.of_finite K _
+  -- „Insbesondere ist das Element m ∈ Z(m) algebraisch
+  --  über K.“
+  have hmem : x ∈ Z⟮x⟯.restrictScalars K :=
+    mem_adjoin_simple_self Z x
+  exact IntermediateField.isAlgebraic_iff.mp
+    (Algebra.IsAlgebraic.isAlgebraic
+      (⟨x, hmem⟩ : Z⟮x⟯.restrictScalars K))
+```
+
+Zwei Details verdienen einen zweiten Blick.  Erstens: `Z⟮x⟯`
+ist eine Erweiterung von $`Z`, aber die Aussage „$`Z(m)/K` ist
+algebraisch“ braucht $`Z(m)` als Erweiterung von $`K` — diesen
+stillschweigenden Wechsel des Grundkörpers, den das Skript gar
+nicht erwähnt, macht `restrictScalars K` explizit.  Zweitens
+steckt im Schritt „$`f ∈ Z[x]` hat $`m` als Nullstelle, also ist
+$`m` algebraisch über $`Z`“ die kleine Rechnung, dass Auswerten
+über $`Z` und Auswerten über $`M` dasselbe ergeben
+(`eval₂_eq_eval_map` und `map_toSubring`).