diff --git a/AlgebraInLean.lean b/AlgebraInLean.lean
index 2f0f575..3cda2da 100644
--- a/AlgebraInLean.lean
+++ b/AlgebraInLean.lean
@@ -5,6 +5,7 @@ import AlgebraInLean.Ideals
 import AlgebraInLean.Polynomials
 import AlgebraInLean.Degrees
 import AlgebraInLean.Elements
+import AlgebraInLean.Transitivity
 import AlgebraInLean.LittleFermat
 import AlgebraInLean.Cauchy
 import AlgebraInLean.Frobenius
diff --git a/AlgebraInLean/Elements.lean b/AlgebraInLean/Elements.lean
index fd7522f..08d68f7 100644
--- a/AlgebraInLean/Elements.lean
+++ b/AlgebraInLean/Elements.lean
@@ -4,8 +4,7 @@ Algebra in Lean — Kapitel 3 des Skripts
 
 Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
 (Stefan Kebekus, CC-BY 4.0).  Sie übersetzt den Satz über den
-Grad eines Elements (satz:3-5-4) und die Transitivität der
-Algebraizität (kor:TdA) nach Lean.
+Grad eines Elements (satz:3-5-4) nach Lean.
 -/
 import Mathlib
 
@@ -14,7 +13,7 @@ namespace AlgebraInLean
 open IntermediateField
 
 /-!
-# Algebraische Elemente und Transitivität
+# Der Grad eines Elements
 
 ## Das Mathlib-Wörterbuch
 
@@ -58,55 +57,23 @@ theorem grad_element {K L : Type*} [Field K] [Field L]
     Fintype.card_fin]
   rfl
 
-/-!
-## Die Transitivität der Algebraizität
-
-Korollar 3.7.1 des Skripts: „Es seien L/K und M/L zwei
-algebraische Körpererweiterungen.  Dann ist auch M/K
-algebraisch.“
-
-Der Kern des Skript-Beweises — adjungiere die endlich vielen
-Koeffizienten des Minimalpolynoms, schließe auf Endlichkeit und
-klettere mit der Gradformel den Turm hinauf — ist in Mathlib
-das Lemma `isIntegral_trans`.
--/
-
-theorem transitivitaet (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 m
-  -- „Wir wissen, dass m algebraisch über L ist“ — über
-  --  Körpern gleichbedeutend: m ist ganz über L.
-  have hm : IsIntegral L m :=
-    (Algebra.IsAlgebraic.isAlgebraic m).isIntegral
-  -- Ebenso ist die algebraische Erweiterung L/K ganz.
-  have : Algebra.IsIntegral K L :=
-    Algebra.IsAlgebraic.isIntegral
-  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und
-  --  die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest
-  --  des Skript-Beweises ist das Lemma isIntegral_trans.
-  exact (isIntegral_trans m hm).isAlgebraic
-
 /-!
 ## Übungsaufgabe
 
-Aus dem Skript: „Die Menge der über K algebraischen Elemente
-von L bildet einen Unterkörper von L, genannt der algebraische
-Abschluss von K im Oberkörper L.“  Die einzelnen
-Abgeschlossenheiten kennt Mathlib als `IsIntegral.add`,
-`IsIntegral.neg`, `IsIntegral.mul`, `IsIntegral.pow` und
-`IsIntegral.inv`.  Die Übung: Kombinieren Sie sie und ersetzen
-Sie das `sorry` durch einen Beweis.
+Das erste Korollar des Skripts zu Satz 3.5.4: „Es sei L/K eine
+Körpererweiterung und es sei a ∈ L.  Falls [a:K] < ∞ ist, dann
+ist K(a) algebraisch über K.“  Die beiden Zutaten kennt Mathlib
+als `IntermediateField.adjoin.finiteDimensional` und
+`Algebra.IsAlgebraic.of_finite`; die Endlichkeit muss mit
+`have := …` in den Kontext geholt werden, damit die
+Instanzsuche sie sieht.  Ersetzen Sie das `sorry` durch einen
+Beweis.
 -/
 
-theorem algebraisch_quadrat {K L : Type*} [Field K]
+theorem einfach_algebraisch {K L : Type*} [Field K]
     [Field L] [Algebra K L] {a : L}
     (ha : IsIntegral K a) :
-    IsIntegral K (a ^ 2 + a) := by
+    Algebra.IsAlgebraic K K⟮a⟯ := by
   sorry
 
 end AlgebraInLean
diff --git a/AlgebraInLean/Transitivity.lean b/AlgebraInLean/Transitivity.lean
new file mode 100644
index 0000000..940cb82
--- /dev/null
+++ b/AlgebraInLean/Transitivity.lean
@@ -0,0 +1,67 @@
+/-
+Algebra in Lean — Kapitel 3 des Skripts
+=======================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt die Transitivität
+der Algebraizität (kor:TdA) nach Lean.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+open IntermediateField
+
+/-!
+# Die Transitivität der Algebraizität
+
+Korollar 3.7.1 des Skripts: „Es seien L/K und M/L zwei
+algebraische Körpererweiterungen.  Dann ist auch M/K
+algebraisch.“
+
+Der Kern des Skript-Beweises — adjungiere die endlich vielen
+Koeffizienten des Minimalpolynoms, schließe auf Endlichkeit und
+klettere mit der Gradformel den Turm hinauf — ist in Mathlib
+das Lemma `isIntegral_trans`.  Das Mathlib-Wörterbuch aus
+`AlgebraInLean/Elements.lean` gilt unverändert weiter.
+-/
+
+theorem transitivitaet (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 m
+  -- „Wir wissen, dass m algebraisch über L ist“ — über
+  --  Körpern gleichbedeutend: m ist ganz über L.
+  have hm : IsIntegral L m :=
+    (Algebra.IsAlgebraic.isAlgebraic m).isIntegral
+  -- Ebenso ist die algebraische Erweiterung L/K ganz.
+  have : Algebra.IsIntegral K L :=
+    Algebra.IsAlgebraic.isIntegral
+  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und
+  --  die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest
+  --  des Skript-Beweises ist das Lemma isIntegral_trans.
+  exact (isIntegral_trans m hm).isAlgebraic
+
+/-!
+## Übungsaufgabe
+
+Aus dem Skript: „Die Menge der über K algebraischen Elemente
+von L bildet einen Unterkörper von L, genannt der algebraische
+Abschluss von K im Oberkörper L.“  Die einzelnen
+Abgeschlossenheiten kennt Mathlib als `IsIntegral.add`,
+`IsIntegral.neg`, `IsIntegral.mul`, `IsIntegral.pow` und
+`IsIntegral.inv`.  Die Übung: Kombinieren Sie sie und ersetzen
+Sie das `sorry` durch einen Beweis.
+-/
+
+theorem algebraisch_quadrat {K L : Type*} [Field K]
+    [Field L] [Algebra K L] {a : L}
+    (ha : IsIntegral K a) :
+    IsIntegral K (a ^ 2 + a) := by
+  sorry
+
+end AlgebraInLean
diff --git a/Book.lean b/Book.lean
index 6029e00..0535880 100644
--- a/Book.lean
+++ b/Book.lean
@@ -8,6 +8,7 @@ import Book.Ideals
 import Book.Polynomials
 import Book.Degrees
 import Book.Elements
+import Book.Transitivity
 import Book.LittleFermat
 import Book.Cauchy
 import Book.Frobenius
@@ -75,6 +76,8 @@ oder der ausführlichen Anleitung am Anfang der
 
 {include 0 Book.Elements}
 
+{include 0 Book.Transitivity}
+
 {include 0 Book.LittleFermat}
 
 {include 0 Book.Cauchy}
diff --git a/Book/Elements.lean b/Book/Elements.lean
index c3625a8..bec85d0 100644
--- a/Book/Elements.lean
+++ b/Book/Elements.lean
@@ -13,18 +13,19 @@ open Verso.Genre.Manual.InlineLean
 set_option pp.rawOnError true
 set_option verso.docstring.allowMissing true
 
-#doc (Manual) "Algebraische Elemente und Transitivität" =>
+#doc (Manual) "Der Grad eines Elements" =>
 %%%
 htmlSplit := .never
 tag := "elemente"
 file := "elemente"
 %%%
 
-Dieses Kapitel übersetzt zwei weitere Resultate aus Kapitel 3 des
-Skripts nach Lean: den Satz über den Grad einer einfachen
-algebraischen Erweiterung, $`[a:K] = [K(a):K]`, und die
-Transitivität der Algebraizität.  Beide bauen auf der Gradformel
-aus dem letzten Kapitel auf.
+Dieses Kapitel übersetzt Satz 3.5.4 des Skripts nach Lean: Für
+ein algebraisches Element $`a` stimmt der Grad $`[a:K]` des
+Minimalpolynoms mit dem Grad $`[K(a):K]` der erzeugten
+Körpererweiterung überein.  Zusammen mit der Gradformel aus dem
+letzten Kapitel ist das das Arbeitspferd für das nächste
+Kapitel, die Transitivität der Algebraizität.
 
 # Das Mathlib-Wörterbuch
 
@@ -51,10 +52,10 @@ aus dem letzten Kapitel auf.
   `Algebra.IsAlgebraic K L`.  Das elementweise Ausbuchstabieren
   übernimmt `Algebra.IsAlgebraic.isAlgebraic`.
 
-# Der Grad eines Elements
+# Satz 3.5.4
 
-Satz 3.5.4 des Skripts verbindet den Grad eines Elements mit dem
-Grad der von ihm erzeugten Körpererweiterung:
+Der Satz verbindet den Grad eines Elements mit dem Grad der von
+ihm erzeugten Körpererweiterung:
 
 > *Satz 3.5.4 (Grad von Körpererweiterungen und Grad von
   Elementen).* Es sei $`L/K` eine Körpererweiterung und es sei
@@ -104,114 +105,32 @@ Mathlibs 0-Konvention steht auf beiden Seiten schlicht 0.  Als
 fertiges Zitat heißt unser Satz übrigens
 `IntermediateField.adjoin.finrank`.
 
-# Die Transitivität der Algebraizität
-
-Das Hauptresultat von Kapitel 3 des Skripts:
-
-> *Korollar 3.7.1 (Transitivität der Algebraizität).* Es seien
-  $`L/K` und $`M/L` zwei algebraische Körpererweiterungen.  Dann
-  ist auch $`M/K` algebraisch.
-
-> _Beweis._ Es sei ein Element $`m ∈ M` gegeben.  Wir wissen,
-  dass $`m` algebraisch über $`L` ist; es sei
-  $`f(x) = λ_0 + λ_1 x + ⋯ + λ_{n-1} x^{n-1} + x^n` das
-  Minimalpolynom von $`m` über $`L`.  Die Koeffizienten $`λ_i`
-  liegen in $`L`.  Betrachte jetzt den Körper
-  $`Z := K(λ_0, …, λ_{n-1})` und die Kette von
-  Körpererweiterungen $`K ⊆ Z ⊆ Z(m) ∋ m`.  Die Erweiterung
-  $`L/K` ist algebraisch, also sind die endlich vielen Elemente
-  $`λ_0, …, λ_{n-1}` allesamt algebraisch über $`K`; deshalb ist
-  $`[Z:K] < ∞`.  Weiter liegt das Polynom $`f` in $`Z[x]` und
-  hat $`m` als Nullstelle.  Also ist $`m` auch algebraisch über
-  $`Z`, und Satz 3.5.4 liefert $`[Z(m):Z] < ∞`.  Mit der
-  Gradformel folgt $`[Z(m):K] = [Z(m):Z]·[Z:K] < ∞`.  Also ist
-  die Erweiterung $`Z(m)/K` algebraisch; insbesondere ist das
-  Element $`m ∈ Z(m)` algebraisch über $`K`.
-
-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;
-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]
-    [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 m
-  -- „Wir wissen, dass m algebraisch über L ist“ — über
-  --  Körpern gleichbedeutend: m ist ganz über L.
-  have hm : IsIntegral L m :=
-    (Algebra.IsAlgebraic.isAlgebraic m).isIntegral
-  -- Ebenso ist die algebraische Erweiterung L/K ganz.
-  have : Algebra.IsIntegral K L :=
-    Algebra.IsAlgebraic.isIntegral
-  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und
-  --  die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest
-  --  des Skript-Beweises ist das Lemma isIntegral_trans.
-  exact (isIntegral_trans m hm).isAlgebraic
-```
-
-Das Skript warnt an dieser Stelle:
-
-> *Warnung (Prüfungsfalle).* Der Satz über die Transitivität der
-  Algebraizität wird in Prüfungen sehr gern gefragt.  Beachten
-  Sie, dass der Beweis ziemlich indirekt ist.  In Prüfungen
-  sehen wir oft, dass Kandidatinnen und Kandidaten für ein
-  gegebenes $`a ∈ M` direkt ein Minimalpolynom konstruieren
-  wollen.  Das hat in der Geschichte der Mathematik noch in
-  keiner Prüfung funktioniert.  Lassen Sie das!
-
-Die Warnung gilt wortgleich in Lean: Auch Mathlib konstruiert
-nirgendwo ein Minimalpolynom von $`m` über $`K` — der Beweis von
-`isIntegral_trans` läuft über die Endlichkeit von Moduln, nicht
-über explizite Polynome.
-
-# Bemerkungen
-
-1. Wer in den Beweis von `isIntegral_trans` hineinschaut, findet
-   die Schritte des Skripts wieder: Dort wird die von den
-   Koeffizienten des Minimalpolynoms erzeugte Unteralgebra
-   gebildet (das $`Z` des Skripts), ihre Endlichkeit als Modul
-   gezeigt, und am Ende die Endlichkeit längs des Turms
-   komponiert — `Module.Finite.trans`, die Gradformel in der
-   Gestalt „endlich über endlich ist endlich“.
-
-2. Als fertiges Zitat ist die Transitivität in Mathlib die
-   Instanz `Algebra.IsAlgebraic.trans K L M` — eine Zeile.
-
 # Übungsaufgabe
 
-Das Skript zieht aus der Transitivität eine schöne Folgerung:
+Das erste Korollar des Skripts zu Satz 3.5.4:
 
-> *Satz und Definition (Algebraischer Abschluss in einem
-  Oberkörper).* Es sei $`L/K` eine Körpererweiterung.  Dann
-  bildet die Menge
-  $`\overline{K} := \{ a ∈ L : a \text{ ist algebraisch über } K \}`
-  einen Unterkörper von $`L`, genannt der _algebraische
-  Abschluss von $`K` im Oberkörper $`L`_.
+> Es sei $`L/K` eine Körpererweiterung und es sei $`a ∈ L`.
+  Falls $`[a:K] < ∞` ist, dann ist $`K(a)` algebraisch
+  über $`K`.
 
-Die einzelnen Abgeschlossenheiten kennt Mathlib als
-`IsIntegral.add`, `IsIntegral.neg`, `IsIntegral.mul`,
-`IsIntegral.pow` und `IsIntegral.inv`.  Die Übung: Kombinieren
-Sie sie.  Öffnen Sie `AlgebraInLean/Elements.lean` und ersetzen
-Sie das `sorry` durch einen Beweis.
+Die beiden Zutaten kennt Mathlib als
+`IntermediateField.adjoin.finiteDimensional` („der Grad ist
+endlich“) und `Algebra.IsAlgebraic.of_finite` („endliche
+Erweiterungen sind algebraisch“).  Beachten Sie, dass die
+Endlichkeit mit `have := …` in den Kontext geholt werden muss,
+damit die Instanzsuche sie sieht.  Öffnen Sie
+`AlgebraInLean/Elements.lean` und ersetzen Sie das `sorry`
+durch einen Beweis.
 
 ```lean
-theorem algebraisch_quadrat {K L : Type*} [Field K]
+theorem einfach_algebraisch {K L : Type*} [Field K]
     [Field L] [Algebra K L] {a : L}
     (ha : IsIntegral K a) :
-    IsIntegral K (a ^ 2 + a) := by
+    Algebra.IsAlgebraic K K⟮a⟯ := by
   sorry
 ```
 
-# Der vollständige Beweis von Satz 3.5.4
+# Der vollständige Beweis
 
 Oben haben wir die eigentliche Arbeit — die Potenzen bilden eine
 Basis von $`K(a)` — bei `IntermediateField.adjoin.powerBasis`
@@ -578,115 +497,3 @@ theorem grad_element_vollstaendig {a : L}
   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`).
diff --git a/Book/Transitivity.lean b/Book/Transitivity.lean
new file mode 100644
index 0000000..f8d6496
--- /dev/null
+++ b/Book/Transitivity.lean
@@ -0,0 +1,246 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`, ermittelt mit
+-- `#min_imports`.
+import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
+import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.RegularLocalRing.Defs
+import Mathlib.RingTheory.SimpleRing.Principal
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Die Transitivität der Algebraizität" =>
+%%%
+htmlSplit := .never
+tag := "transitivitaet"
+file := "transitivitaet"
+%%%
+
+Dieses Kapitel übersetzt das Hauptresultat von Kapitel 3 des
+Skripts nach Lean: die Transitivität der Algebraizität.  Der
+Beweis kombiniert die Gradformel mit dem Satz über den Grad
+eines Elements; das Mathlib-Wörterbuch des letzten Kapitels
+gilt unverändert weiter.
+
+# Korollar 3.7.1
+
+> *Korollar 3.7.1 (Transitivität der Algebraizität).* Es seien
+  $`L/K` und $`M/L` zwei algebraische Körpererweiterungen.  Dann
+  ist auch $`M/K` algebraisch.
+
+> _Beweis._ Es sei ein Element $`m ∈ M` gegeben.  Wir wissen,
+  dass $`m` algebraisch über $`L` ist; es sei
+  $`f(x) = λ_0 + λ_1 x + ⋯ + λ_{n-1} x^{n-1} + x^n` das
+  Minimalpolynom von $`m` über $`L`.  Die Koeffizienten $`λ_i`
+  liegen in $`L`.  Betrachte jetzt den Körper
+  $`Z := K(λ_0, …, λ_{n-1})` und die Kette von
+  Körpererweiterungen $`K ⊆ Z ⊆ Z(m) ∋ m`.  Die Erweiterung
+  $`L/K` ist algebraisch, also sind die endlich vielen Elemente
+  $`λ_0, …, λ_{n-1}` allesamt algebraisch über $`K`; deshalb ist
+  $`[Z:K] < ∞`.  Weiter liegt das Polynom $`f` in $`Z[x]` und
+  hat $`m` als Nullstelle.  Also ist $`m` auch algebraisch über
+  $`Z`, und Satz 3.5.4 liefert $`[Z(m):Z] < ∞`.  Mit der
+  Gradformel folgt $`[Z(m):K] = [Z(m):Z]·[Z:K] < ∞`.  Also ist
+  die Erweiterung $`Z(m)/K` algebraisch; insbesondere ist das
+  Element $`m ∈ Z(m)` algebraisch über $`K`.
+
+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;
+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]
+    [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 m
+  -- „Wir wissen, dass m algebraisch über L ist“ — über
+  --  Körpern gleichbedeutend: m ist ganz über L.
+  have hm : IsIntegral L m :=
+    (Algebra.IsAlgebraic.isAlgebraic m).isIntegral
+  -- Ebenso ist die algebraische Erweiterung L/K ganz.
+  have : Algebra.IsIntegral K L :=
+    Algebra.IsAlgebraic.isIntegral
+  -- „Betrachte jetzt den Körper Z := K(λ₀, …, λ_{n-1}) und
+  --  die Kette K ⊆ Z ⊆ Z(m) ∋ m …“ — der gesamte Rest
+  --  des Skript-Beweises ist das Lemma isIntegral_trans.
+  exact (isIntegral_trans m hm).isAlgebraic
+```
+
+Das Skript warnt an dieser Stelle:
+
+> *Warnung (Prüfungsfalle).* Der Satz über die Transitivität der
+  Algebraizität wird in Prüfungen sehr gern gefragt.  Beachten
+  Sie, dass der Beweis ziemlich indirekt ist.  In Prüfungen
+  sehen wir oft, dass Kandidatinnen und Kandidaten für ein
+  gegebenes $`a ∈ M` direkt ein Minimalpolynom konstruieren
+  wollen.  Das hat in der Geschichte der Mathematik noch in
+  keiner Prüfung funktioniert.  Lassen Sie das!
+
+Die Warnung gilt wortgleich in Lean: Auch Mathlib konstruiert
+nirgendwo ein Minimalpolynom von $`m` über $`K` — der Beweis von
+`isIntegral_trans` läuft über die Endlichkeit von Moduln, nicht
+über explizite Polynome.
+
+# Bemerkungen
+
+1. Wer in den Beweis von `isIntegral_trans` hineinschaut, findet
+   die Schritte des Skripts wieder: Dort wird die von den
+   Koeffizienten des Minimalpolynoms erzeugte Unteralgebra
+   gebildet (das $`Z` des Skripts), ihre Endlichkeit als Modul
+   gezeigt, und am Ende die Endlichkeit längs des Turms
+   komponiert — `Module.Finite.trans`, die Gradformel in der
+   Gestalt „endlich über endlich ist endlich“.
+
+2. Als fertiges Zitat ist die Transitivität in Mathlib die
+   Instanz `Algebra.IsAlgebraic.trans K L M` — eine Zeile.
+
+# Übungsaufgabe
+
+Das Skript zieht aus der Transitivität eine schöne Folgerung:
+
+> *Satz und Definition (Algebraischer Abschluss in einem
+  Oberkörper).* Es sei $`L/K` eine Körpererweiterung.  Dann
+  bildet die Menge
+  $`\overline{K} := \{ a ∈ L : a \text{ ist algebraisch über } K \}`
+  einen Unterkörper von $`L`, genannt der _algebraische
+  Abschluss von $`K` im Oberkörper $`L`_.
+
+Die einzelnen Abgeschlossenheiten kennt Mathlib als
+`IsIntegral.add`, `IsIntegral.neg`, `IsIntegral.mul`,
+`IsIntegral.pow` und `IsIntegral.inv`.  Die Übung: Kombinieren
+Sie sie.  Öffnen Sie `AlgebraInLean/Transitivity.lean` und
+ersetzen Sie das `sorry` durch einen Beweis.
+
+```lean
+theorem algebraisch_quadrat {K L : Type*} [Field K]
+    [Field L] [Algebra K L] {a : L}
+    (ha : IsIntegral K a) :
+    IsIntegral K (a ^ 2 + a) := by
+  sorry
+```
+
+# Der vollständige Beweis
+
+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
+open Polynomial IntermediateField
+
+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`).