diff --git a/AlgebraInLean.lean b/AlgebraInLean.lean
index cebbd62..4db408f 100644
--- a/AlgebraInLean.lean
+++ b/AlgebraInLean.lean
@@ -1,5 +1,7 @@
 -- Wurzelmodul: importiert alle Übungsdateien.
 import AlgebraInLean.Basics
 import AlgebraInLean.Quotients
+import AlgebraInLean.Ideals
+import AlgebraInLean.Polynomials
 import AlgebraInLean.LittleFermat
 import AlgebraInLean.Cauchy
diff --git a/AlgebraInLean/Ideals.lean b/AlgebraInLean/Ideals.lean
new file mode 100644
index 0000000..8d7459f
--- /dev/null
+++ b/AlgebraInLean/Ideals.lean
@@ -0,0 +1,143 @@
+/-
+Algebra in Lean — Kapitel 9 des Skripts
+=======================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt den Satz „ℤ ist
+ein Hauptidealring“ (satz:9-1-4) Satz für Satz nach Lean —
+der klassische Beweis über Division mit Rest.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+/-!
+# Ringe und Ideale
+
+## Das Mathlib-Wörterbuch
+
+* Ein Ideal in einem kommutativen Ring `R` ist ein Term
+  `I : Ideal R`.  Die beiden Bedingungen aus der
+  Ideal-Definition des Skripts heißen `I.add_mem` (für alle a, b ∈ I
+  ist a+b ∈ I) und `I.mul_mem_left` (für alle r ∈ R und
+  a ∈ I ist r·a ∈ I); außerdem ist `I.zero_mem : 0 ∈ I`.
+
+* Das von einer Menge `s` erzeugte Ideal ist `Ideal.span s`;
+  ein *Hauptideal* (a) ist also `Ideal.span {a}`.  Die
+  Beobachtung „Hauptideale und Teilbarkeit“ des Skripts ist
+  das Lemma `Ideal.mem_span_singleton : b ∈ span {a} ↔
+  a ∣ b`.
+
+* „Jedes Ideal ist endlich erzeugt / ein Hauptideal“ sind
+  die Prädikate `IsNoetherianRing R` und
+  `IsPrincipalIdealRing R`.
+
+## ℤ ist ein Hauptidealring
+
+Der Satz „ℤ ist ein Hauptidealring“ aus Kapitel 9 des
+Skripts, mit Beweis:
+
+„Es sei I ⊂ ℤ ein Ideal und I ≠ {0}.  Dann gibt es ein
+x ∈ I∖{0}.  Beachte, dass dann auch −x = (−1)·x in I ist.
+Also enthält I positive Elemente.  Sei a ∈ I jetzt das
+kleinste positive Element.  Wir werden zeigen, dass I = (a)
+ist.  Die Inklusion (a) ⊆ I ist klar.  Sei b ∈ I irgendein
+positives Element, dann teilen wir mit Rest: b = q·a + r
+mit 0 ≤ r < a.  Die Zahl r ist jetzt aber in I, denn b und
+q·a sind in I.  Weiter muss wegen der Minimalität von a
+also r = 0 sein und somit b ∈ (a).“
+
+Zwei Anmerkungen zur Übersetzung.  Das „kleinste positive
+Element“ liefert das Wohlordnungsprinzip, in Mathlib
+`Int.exists_least_of_bdd`.  Und wo das Skript nur positive
+b behandelt (und den Rest dem Leser überlässt), nehmen wir
+gleich beliebige b — die Division mit Rest in Lean
+funktioniert für alle ganzen Zahlen.
+-/
+
+theorem int_hauptidealring (I : Ideal ℤ) :
+    ∃ a : ℤ, I = Ideal.span {a} := by
+  -- „… und I ≠ {0}.“  Das Nullideal erledigt a = 0:
+  by_cases hI : I = ⊥
+  · exact ⟨0, by simp [hI]⟩
+  -- „Dann gibt es ein x ∈ I∖{0}.“
+  · obtain ⟨x, hxI, hx0⟩ :=
+      Submodule.exists_mem_ne_zero_of_ne_bot hI
+    -- „Beachte, dass dann auch −x = (−1)·x in I ist.  Also
+    --  enthält I positive Elemente.“
+    have hmx : -x ∈ I := by
+      have h := I.mul_mem_left (-1) hxI
+      simpa using h
+    have hpos : ∃ y, y ∈ I ∧ 0 < y := by
+      rcases lt_or_gt_of_ne hx0 with h | h
+      · exact ⟨-x, hmx, by omega⟩
+      · exact ⟨x, hxI, h⟩
+    -- „Sei a ∈ I jetzt das kleinste positive Element.“
+    obtain ⟨a, ⟨haI, ha⟩, hmin⟩ :=
+      Int.exists_least_of_bdd
+        (P := fun y => y ∈ I ∧ 0 < y)
+        ⟨1, fun z hz => by have := hz.2; omega⟩ hpos
+    -- „Wir werden zeigen, dass I = (a) ist.“
+    refine ⟨a, le_antisymm ?_ ?_⟩
+    · -- „Sei b ∈ I irgendein Element, dann teilen wir mit
+      --  Rest: b = q·a + r mit 0 ≤ r < a.“
+      intro b hb
+      set q := b / a with hq_def
+      set r := b % a with hr_def
+      have hdiv : b = a * q + r := by
+        rw [hq_def, hr_def]
+        exact (Int.mul_ediv_add_emod b a).symm
+      have hr0 : 0 ≤ r := Int.emod_nonneg b (by omega)
+      have hra : r < a := Int.emod_lt_of_pos b ha
+      -- „Die Zahl r ist jetzt aber in I, denn b und q·a
+      --  sind in I.“
+      have hqaI : a * q ∈ I := I.mul_mem_right q haI
+      have hrI : r ∈ I := by
+        have hr_eq : r = b - a * q := by rw [hdiv]; ring
+        rw [hr_eq]
+        exact I.sub_mem hb hqaI
+      -- „Weiter muss wegen der Minimalität von a also r = 0
+      --  sein …“
+      have hr : r = 0 := by
+        by_contra hr
+        have : a ≤ r := hmin r ⟨hrI, by omega⟩
+        omega
+      -- „… und somit b ∈ (a).“
+      rw [Ideal.mem_span_singleton]
+      exact ⟨q, by rw [hdiv, hr]; ring⟩
+    · -- „Die Inklusion (a) ⊆ I ist klar.“
+      rw [Ideal.span_le, Set.singleton_subset_iff]
+      exact haI
+
+/-!
+## Bemerkungen
+
+1. In Mathlib ist `IsPrincipalIdealRing ℤ` eine Instanz:
+   ℤ ist ein euklidischer Ring, und
+   `EuclideanDomain.to_principal_ideal_domain` führt genau
+   unser Argument für beliebige euklidische Ringe.  Damit
+   ist auch Satz 9.3.8 des Skripts abgedeckt: K[x] ist
+   euklidisch (Division mit Rest, wobei der Grad die Rolle
+   des Betrags übernimmt), also ein Hauptidealring.
+
+2. Auch der Hilbertsche Basissatz aus diesem Kapitel steht
+   in Mathlib: `Polynomial.isNoetherianRing`.
+
+## Übungsaufgabe
+
+Das Beispiel „Triviale Ideale“ des Skripts: „Wenn R ein
+Körper und I ⊂ R ein Ideal ist und a ∈ I∖{0}, dann ist auch
+jedes andere Körperelement in I.  Sei nämlich irgendein
+Element r ∈ R gegeben.  Nach Definition ist
+r = (r·a⁻¹)·a ∈ I.  Also ist I = R.“  Übersetzen Sie dieses
+Argument: Ersetzen Sie das `sorry` durch einen Beweis.
+Tipp: Die Taktik `field_simp` räumt Brüche auf; sie benutzt
+dabei die Hypothese `ha0` automatisch.
+-/
+
+theorem ideal_im_koerper {K : Type*} [Field K]
+    (I : Ideal K) {a : K} (haI : a ∈ I) (ha0 : a ≠ 0)
+    (r : K) : r ∈ I := by
+  sorry
+
+end AlgebraInLean
diff --git a/AlgebraInLean/Polynomials.lean b/AlgebraInLean/Polynomials.lean
new file mode 100644
index 0000000..0c58066
--- /dev/null
+++ b/AlgebraInLean/Polynomials.lean
@@ -0,0 +1,140 @@
+/-
+Algebra in Lean — Kapitel 7 des Skripts
+=======================================
+
+Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
+(Stefan Kebekus, CC-BY 4.0).  Sie übersetzt die beiden
+Beispiele nach dem Eisenstein-Kriterium
+(Satz_Eisenstein_Kriterium) nach Lean; das Kriterium selbst
+zitieren wir aus Mathlib.
+-/
+import Mathlib
+
+namespace AlgebraInLean
+
+open Polynomial
+
+/-!
+# Polynome und Irreduzibilität
+
+## Das Mathlib-Wörterbuch
+
+* Der Polynomring über `R` heißt `Polynomial R`, mit der
+  Notation `R[X]`.  Die Variable ist `X`, das konstante
+  Polynom zu `a : R` ist `C a`; ein Polynom wie x³−2 schreibt
+  sich also `X ^ 3 - C 2`.
+
+* Der k-te Koeffizient ist `f.coeff k`, der Grad `f.degree`.
+  Achtung: `degree` hat Werte in `WithBot ℕ` — das
+  Nullpolynom bekommt den Grad ⊥ („minus unendlich“, wie im
+  Skript).  Daneben gibt es `f.natDegree : ℕ`.
+
+* „f ist normiert“ (Leitkoeffizient 1) ist `f.Monic`;
+  „f ist irreduzibel“ ist `Irreducible f`; die Bedingung
+  „ggT der Koeffizienten ist 1“ aus dem Eisenstein-Kriterium
+  heißt `f.IsPrimitive` (kein Nichteinheits-Teiler in R).
+
+## Das Eisenstein-Kriterium
+
+Der Satz aus Kapitel 7 des Skripts:
+
+**Satz (Eisenstein-Kriterium).**  *Es sei R ein faktorieller
+Ring und es sei f = a₀ + a₁·x + … + aₙ·xⁿ ∈ R[x] ein Polynom
+vom Grad n > 0.  Weiter sei ggT(a₀, …, aₙ) = 1.  Wenn es ein
+Primelement p ∈ R gibt mit p|a₀, p|a₁, …, p|a_{n−1} und
+p² ∤ a₀, dann ist f irreduzibel in R[x].*
+
+In Mathlib heißt der Satz
+`Polynomial.irreducible_of_eisenstein_criterion`.  Er ist
+dort über ein Primideal P statt eines Primelements p
+formuliert — für uns ist P das Hauptideal (p) aus dem
+letzten Kapitel, und „p teilt aₖ“ wird zu
+`f.coeff k ∈ Ideal.span {p}`.  Statt „p ∤ aₙ“ (was im Skript
+aus ggT = 1 folgt) verlangt Mathlib direkt
+`f.leadingCoeff ∉ P`.
+
+## Erstes Beispiel: xⁿ − r
+
+„Das Polynom xⁿ − r ∈ ℤ[x] ist irreduzibel, wenn r durch
+eine Primzahl p, aber nicht durch p² teilbar ist.“
+
+Das Skript lässt die Kontrolle der Eisenstein-Bedingungen
+als Kopfrechnung weg — in Lean führen wir sie aus und lernen
+dabei die Koeffizienten-API kennen: `coeff_sub`,
+`coeff_X_pow` und `coeff_C` berechnen die Koeffizienten von
+xⁿ − r, nämlich aₙ = 1, a₀ = −r und aₖ = 0 sonst.
+-/
+
+theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
+    (p : ℕ) (hp : p.Prime) (hpr : (p : ℤ) ∣ r)
+    (hp2r : ¬ (p : ℤ) ^ 2 ∣ r) :
+    Irreducible (X ^ n - C r) := by
+  -- Das Primelement p des Skripts wird zum Primideal (p):
+  have hprime : Prime (p : ℤ) :=
+    Nat.prime_iff_prime_int.mp hp
+  have hP : (Ideal.span {(p : ℤ)}).IsPrime :=
+    (Ideal.span_singleton_prime hprime.ne_zero).mpr hprime
+  -- Grad und Leitkoeffizient von f = xⁿ − r:
+  have hmonic : (X ^ n - C r).Monic :=
+    monic_X_pow_sub_C r hn.ne'
+  have hdeg := degree_X_pow_sub_C hn r
+  apply irreducible_of_eisenstein_criterion hP
+  -- „p ∤ aₙ“: Der Leitkoeffizient ist 1, und p ∤ 1, weil
+  -- p keine Einheit ist.
+  · rw [hmonic.leadingCoeff, Ideal.mem_span_singleton]
+    exact fun h => hprime.not_isUnit (isUnit_of_dvd_one h)
+  -- „p|a₀, …, p|a_{n−1}“: Unterhalb von Grad n sind die
+  -- Koeffizienten −r (bei k = 0) und 0 (sonst) — beide
+  -- durch p teilbar.
+  · intro k hk
+    have hkn : k < n := by
+      rw [hdeg] at hk
+      exact_mod_cast hk
+    rw [coeff_sub, coeff_X_pow, if_neg hkn.ne, coeff_C,
+      Ideal.mem_span_singleton]
+    rcases eq_or_ne k 0 with h0 | h0
+    · subst h0
+      simpa using hpr
+    · simp [h0]
+  -- „… vom Grad n > 0.“
+  · rw [hdeg]
+    exact_mod_cast hn
+  -- „p² ∤ a₀“: Der konstante Koeffizient ist −r.
+  · rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton,
+      coeff_sub, coeff_X_pow, if_neg hn.ne, coeff_C,
+      if_pos rfl, zero_sub, dvd_neg]
+    exact hp2r
+  -- „ggT(a₀, …, aₙ) = 1“: f ist normiert, also primitiv.
+  · exact hmonic.isPrimitive
+
+/-!
+## Bemerkungen
+
+1. Mathlibs Beweis des Eisenstein-Kriteriums folgt derselben
+   Idee wie das Erklärvideo 9-1: Reduktion der Koeffizienten
+   modulo p.  Auch das Gauß-Kriterium aus dem ersten Teil
+   des Kapitels steht in Mathlib (Datei
+   `Mathlib.RingTheory.Polynomial.GaussLemma`).
+
+2. Das zweite Beispiel des Skripts — xⁿ − p ist irreduzibel
+   und deshalb das Minimalpolynom von ⁿ√p — greifen wir im
+   Kapitel über Körpererweiterungen wieder auf.
+
+## Übungsaufgabe
+
+Genau dieses zweite Beispiel ist die Übung: „Das Polynom
+xⁿ − p ∈ ℤ[x] ist für jede Primzahl p irreduzibel.“  Wenden
+Sie `xn_sub_r_irreduzibel` mit r = p an.  Zu zeigen bleibt
+p² ∤ p: Aus p = p²·c folgt durch Kürzen 1 = p·c — dann wäre
+p eine Einheit, im Widerspruch zur Primalität.  Nützlich
+sind `mul_left_cancel₀`, `isUnit_of_dvd_one` und
+`Prime.not_isUnit`.  Ersetzen Sie das `sorry` durch einen
+Beweis.
+-/
+
+theorem xn_sub_p_irreduzibel (n : ℕ) (hn : 0 < n) (p : ℕ)
+    (hp : p.Prime) :
+    Irreducible (X ^ n - C (p : ℤ)) := by
+  sorry
+
+end AlgebraInLean
diff --git a/Book.lean b/Book.lean
index e7d7a34..096a172 100644
--- a/Book.lean
+++ b/Book.lean
@@ -4,6 +4,8 @@ import VersoManual
 
 import Book.Basics
 import Book.Quotients
+import Book.Ideals
+import Book.Polynomials
 import Book.LittleFermat
 import Book.Cauchy
 
@@ -60,6 +62,10 @@ oder der ausführlichen Anleitung am Anfang der
 
 {include 0 Book.Quotients}
 
+{include 0 Book.Ideals}
+
+{include 0 Book.Polynomials}
+
 {include 0 Book.LittleFermat}
 
 {include 0 Book.Cauchy}
diff --git a/Book/Ideals.lean b/Book/Ideals.lean
new file mode 100644
index 0000000..153d70b
--- /dev/null
+++ b/Book/Ideals.lean
@@ -0,0 +1,150 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`: ermittelt mit
+-- `#min_imports`, ergänzt um die Taktiken `ring` und
+-- `field_simp`.
+import Mathlib.Data.Int.LeastGreatest
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.FieldSimp
+
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Ringe und Ideale" =>
+%%%
+htmlSplit := .never
+tag := "ideale"
+%%%
+
+Dieses Kapitel übersetzt den Satz „ℤ ist ein Hauptidealring“ aus
+Kapitel 9 des Skripts — der klassische Beweis über Division mit Rest,
+und zugleich unsere erste Begegnung mit dem Wohlordnungsprinzip in
+Lean.
+
+# Das Mathlib-Wörterbuch
+
+* Ein Ideal in einem kommutativen Ring `R` ist ein Term
+  `I : Ideal R`.  Die beiden Bedingungen aus der Ideal-Definition des
+  Skripts heißen `I.add_mem` (für alle `a, b ∈ I` ist `a+b ∈ I`) und
+  `I.mul_mem_left` (für alle `r ∈ R` und `a ∈ I` ist `r·a ∈ I`);
+  außerdem ist `I.zero_mem : 0 ∈ I`.
+
+* Das von einer Menge `s` erzeugte Ideal ist `Ideal.span s`; ein
+  _Hauptideal_ `(a)` ist also `Ideal.span {a}`.  Die Beobachtung
+  „Hauptideale und Teilbarkeit“ des Skripts ist das Lemma
+  `Ideal.mem_span_singleton : b ∈ span {a} ↔ a ∣ b`.
+
+* „Jedes Ideal ist endlich erzeugt / ein Hauptideal“ sind die
+  Prädikate `IsNoetherianRing R` und `IsPrincipalIdealRing R`.
+
+# ℤ ist ein Hauptidealring
+
+Der Satz aus Kapitel 9 des Skripts, mit Beweis:
+
+> Es sei `I ⊂ ℤ` ein Ideal und `I ≠ {0}`.  Dann gibt es ein
+> `x ∈ I∖{0}`.  Beachte, dass dann auch `−x = (−1)·x` in `I` ist.
+> Also enthält `I` positive Elemente.  Sei `a ∈ I` jetzt das kleinste
+> positive Element.  Wir werden zeigen, dass `I = (a)` ist.  Die
+> Inklusion `(a) ⊆ I` ist klar.  Sei `b ∈ I` irgendein positives
+> Element, dann teilen wir mit Rest: `b = q·a + r` mit `0 ≤ r < a`.
+> Die Zahl `r` ist jetzt aber in `I`, denn `b` und `q·a` sind in `I`.
+> Weiter muss wegen der Minimalität von `a` also `r = 0` sein und
+> somit `b ∈ (a)`.
+
+Zwei Anmerkungen zur Übersetzung.  Das „kleinste positive Element“
+liefert das Wohlordnungsprinzip, in Mathlib
+`Int.exists_least_of_bdd`.  Und wo das Skript nur positive `b`
+behandelt (und den Rest dem Leser überlässt), nehmen wir gleich
+beliebige `b` — die Division mit Rest in Lean funktioniert für alle
+ganzen Zahlen.
+
+```lean
+theorem int_hauptidealring (I : Ideal ℤ) :
+    ∃ a : ℤ, I = Ideal.span {a} := by
+  -- „… und I ≠ {0}.“  Das Nullideal erledigt a = 0:
+  by_cases hI : I = ⊥
+  · exact ⟨0, by simp [hI]⟩
+  -- „Dann gibt es ein x ∈ I∖{0}.“
+  · obtain ⟨x, hxI, hx0⟩ :=
+      Submodule.exists_mem_ne_zero_of_ne_bot hI
+    -- „Beachte, dass dann auch −x = (−1)·x in I ist.  Also
+    --  enthält I positive Elemente.“
+    have hmx : -x ∈ I := by
+      have h := I.mul_mem_left (-1) hxI
+      simpa using h
+    have hpos : ∃ y, y ∈ I ∧ 0 < y := by
+      rcases lt_or_gt_of_ne hx0 with h | h
+      · exact ⟨-x, hmx, by omega⟩
+      · exact ⟨x, hxI, h⟩
+    -- „Sei a ∈ I jetzt das kleinste positive Element.“
+    obtain ⟨a, ⟨haI, ha⟩, hmin⟩ :=
+      Int.exists_least_of_bdd
+        (P := fun y => y ∈ I ∧ 0 < y)
+        ⟨1, fun z hz => by have := hz.2; omega⟩ hpos
+    -- „Wir werden zeigen, dass I = (a) ist.“
+    refine ⟨a, le_antisymm ?_ ?_⟩
+    · -- „Sei b ∈ I irgendein Element, dann teilen wir mit
+      --  Rest: b = q·a + r mit 0 ≤ r < a.“
+      intro b hb
+      set q := b / a with hq_def
+      set r := b % a with hr_def
+      have hdiv : b = a * q + r := by
+        rw [hq_def, hr_def]
+        exact (Int.mul_ediv_add_emod b a).symm
+      have hr0 : 0 ≤ r := Int.emod_nonneg b (by omega)
+      have hra : r < a := Int.emod_lt_of_pos b ha
+      -- „Die Zahl r ist jetzt aber in I, denn b und q·a
+      --  sind in I.“
+      have hqaI : a * q ∈ I := I.mul_mem_right q haI
+      have hrI : r ∈ I := by
+        have hr_eq : r = b - a * q := by rw [hdiv]; ring
+        rw [hr_eq]
+        exact I.sub_mem hb hqaI
+      -- „Weiter muss wegen der Minimalität von a also r = 0
+      --  sein …“
+      have hr : r = 0 := by
+        by_contra hr
+        have : a ≤ r := hmin r ⟨hrI, by omega⟩
+        omega
+      -- „… und somit b ∈ (a).“
+      rw [Ideal.mem_span_singleton]
+      exact ⟨q, by rw [hdiv, hr]; ring⟩
+    · -- „Die Inklusion (a) ⊆ I ist klar.“
+      rw [Ideal.span_le, Set.singleton_subset_iff]
+      exact haI
+```
+
+# Bemerkungen
+
+In Mathlib ist `IsPrincipalIdealRing ℤ` eine Instanz: ℤ ist ein
+euklidischer Ring, und `EuclideanDomain.to_principal_ideal_domain`
+führt genau unser Argument für beliebige euklidische Ringe.  Damit
+ist auch der zweite Satz des Skript-Abschnitts abgedeckt: `K[x]` ist
+euklidisch (Division mit Rest, wobei der Grad die Rolle des Betrags
+übernimmt), also ein Hauptidealring.  Auch der Hilbertsche Basissatz
+aus diesem Kapitel steht in Mathlib: `Polynomial.isNoetherianRing`.
+
+# Übungsaufgabe
+
+Das Beispiel „Triviale Ideale“ des Skripts:
+
+> Wenn `R` ein Körper und `I ⊂ R` ein Ideal ist und `a ∈ I∖{0}`,
+> dann ist auch jedes andere Körperelement in `I`.  Sei nämlich
+> irgendein Element `r ∈ R` gegeben.  Nach Definition ist
+> `r = (r·a⁻¹)·a ∈ I`.  Also ist `I = R`.
+
+Übersetzen Sie dieses Argument: Öffnen Sie
+`AlgebraInLean/Ideals.lean` und ersetzen Sie das `sorry` durch einen
+Beweis.  Tipp: Die Taktik `field_simp` räumt Brüche auf; sie benutzt
+dabei die Hypothese `ha0` automatisch.
+
+```lean
+theorem ideal_im_koerper {K : Type*} [Field K]
+    (I : Ideal K) {a : K} (haI : a ∈ I) (ha0 : a ≠ 0)
+    (r : K) : r ∈ I := by
+  sorry
+```
diff --git a/Book/Polynomials.lean b/Book/Polynomials.lean
new file mode 100644
index 0000000..dae10d9
--- /dev/null
+++ b/Book/Polynomials.lean
@@ -0,0 +1,144 @@
+import VersoManual
+import Manual.Meta
+-- Minimal-Imports statt `import Mathlib`, ermittelt mit
+-- `#min_imports`.
+import Mathlib.Data.Nat.Prime.Int
+import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+#doc (Manual) "Polynome und Irreduzibilität" =>
+%%%
+htmlSplit := .never
+tag := "polynome"
+%%%
+
+Dieses Kapitel übersetzt die beiden Beispiele nach dem
+Eisenstein-Kriterium aus Kapitel 7 des Skripts nach Lean; das
+Kriterium selbst zitieren wir aus Mathlib.  Nebenbei lernen wir die
+Polynom-API kennen.
+
+# Das Mathlib-Wörterbuch
+
+* Der Polynomring über `R` heißt `Polynomial R`, mit der Notation
+  `R[X]`.  Die Variable ist `X`, das konstante Polynom zu `a : R` ist
+  `C a`; ein Polynom wie `x³−2` schreibt sich also `X ^ 3 - C 2`.
+
+* Der k-te Koeffizient ist `f.coeff k`, der Grad `f.degree`.
+  Achtung: `degree` hat Werte in `WithBot ℕ` — das Nullpolynom
+  bekommt den Grad `⊥` („minus unendlich“, wie im Skript).  Daneben
+  gibt es `f.natDegree : ℕ`.
+
+* „f ist normiert“ (Leitkoeffizient 1) ist `f.Monic`; „f ist
+  irreduzibel“ ist `Irreducible f`; die Bedingung „ggT der
+  Koeffizienten ist 1“ aus dem Eisenstein-Kriterium heißt
+  `f.IsPrimitive` (kein Nichteinheits-Teiler in `R`).
+
+# Das Eisenstein-Kriterium
+
+Der Satz aus Kapitel 7 des Skripts:
+
+> *Satz (Eisenstein-Kriterium).* Es sei `R` ein faktorieller Ring und
+> es sei `f = a₀ + a₁·x + … + aₙ·xⁿ ∈ R[x]` ein Polynom vom Grad
+> `n > 0`.  Weiter sei `ggT(a₀, …, aₙ) = 1`.  Wenn es ein Primelement
+> `p ∈ R` gibt mit `p|a₀`, `p|a₁`, …, `p|a_{n−1}` und `p² ∤ a₀`, dann
+> ist `f` irreduzibel in `R[x]`.
+
+In Mathlib heißt der Satz
+`Polynomial.irreducible_of_eisenstein_criterion`.  Er ist dort über
+ein Primideal `P` statt eines Primelements `p` formuliert — für uns
+ist `P` das Hauptideal `(p)` aus dem letzten Kapitel, und „`p` teilt
+`aₖ`“ wird zu `f.coeff k ∈ Ideal.span {p}`.  Statt „`p ∤ aₙ`“ (was im
+Skript aus `ggT = 1` folgt) verlangt Mathlib direkt
+`f.leadingCoeff ∉ P`.
+
+# Erstes Beispiel: xⁿ − r
+
+> Das Polynom `xⁿ − r ∈ ℤ[x]` ist irreduzibel, wenn `r` durch eine
+> Primzahl `p`, aber nicht durch `p²` teilbar ist.
+
+Das Skript lässt die Kontrolle der Eisenstein-Bedingungen als
+Kopfrechnung weg — in Lean führen wir sie aus und lernen dabei die
+Koeffizienten-API kennen: `coeff_sub`, `coeff_X_pow` und `coeff_C`
+berechnen die Koeffizienten von `xⁿ − r`, nämlich `aₙ = 1`, `a₀ = −r`
+und `aₖ = 0` sonst.
+
+```lean
+open Polynomial
+
+theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
+    (p : ℕ) (hp : p.Prime) (hpr : (p : ℤ) ∣ r)
+    (hp2r : ¬ (p : ℤ) ^ 2 ∣ r) :
+    Irreducible (X ^ n - C r) := by
+  -- Das Primelement p des Skripts wird zum Primideal (p):
+  have hprime : Prime (p : ℤ) :=
+    Nat.prime_iff_prime_int.mp hp
+  have hP : (Ideal.span {(p : ℤ)}).IsPrime :=
+    (Ideal.span_singleton_prime hprime.ne_zero).mpr hprime
+  -- Grad und Leitkoeffizient von f = xⁿ − r:
+  have hmonic : (X ^ n - C r).Monic :=
+    monic_X_pow_sub_C r hn.ne'
+  have hdeg := degree_X_pow_sub_C hn r
+  apply irreducible_of_eisenstein_criterion hP
+  -- „p ∤ aₙ“: Der Leitkoeffizient ist 1, und p ∤ 1, weil
+  -- p keine Einheit ist.
+  · rw [hmonic.leadingCoeff, Ideal.mem_span_singleton]
+    exact fun h => hprime.not_isUnit (isUnit_of_dvd_one h)
+  -- „p|a₀, …, p|a_{n−1}“: Unterhalb von Grad n sind die
+  -- Koeffizienten −r (bei k = 0) und 0 (sonst) — beide
+  -- durch p teilbar.
+  · intro k hk
+    have hkn : k < n := by
+      rw [hdeg] at hk
+      exact_mod_cast hk
+    rw [coeff_sub, coeff_X_pow, if_neg hkn.ne, coeff_C,
+      Ideal.mem_span_singleton]
+    rcases eq_or_ne k 0 with h0 | h0
+    · subst h0
+      simpa using hpr
+    · simp [h0]
+  -- „… vom Grad n > 0.“
+  · rw [hdeg]
+    exact_mod_cast hn
+  -- „p² ∤ a₀“: Der konstante Koeffizient ist −r.
+  · rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton,
+      coeff_sub, coeff_X_pow, if_neg hn.ne, coeff_C,
+      if_pos rfl, zero_sub, dvd_neg]
+    exact hp2r
+  -- „ggT(a₀, …, aₙ) = 1“: f ist normiert, also primitiv.
+  · exact hmonic.isPrimitive
+```
+
+# Bemerkungen
+
+Mathlibs Beweis des Eisenstein-Kriteriums folgt derselben Idee wie
+das Erklärvideo 9-1 des Skripts: Reduktion der Koeffizienten modulo
+`p`.  Auch das Gauß-Kriterium aus dem ersten Teil des Kapitels steht
+in Mathlib (Datei `Mathlib.RingTheory.Polynomial.GaussLemma`).  Das
+zweite Beispiel des Skripts — `xⁿ − p` ist irreduzibel und deshalb
+das Minimalpolynom von `ⁿ√p` — greifen wir im Kapitel über
+Körpererweiterungen wieder auf.
+
+# Übungsaufgabe
+
+Genau dieses zweite Beispiel ist die Übung:
+
+> Das Polynom `xⁿ − p ∈ ℤ[x]` ist für jede Primzahl `p` irreduzibel.
+
+Wenden Sie `xn_sub_r_irreduzibel` mit `r = p` an.  Zu zeigen bleibt
+`p² ∤ p`: Aus `p = p²·c` folgt durch Kürzen `1 = p·c` — dann wäre `p`
+eine Einheit, im Widerspruch zur Primalität.  Nützlich sind
+`mul_left_cancel₀`, `isUnit_of_dvd_one` und `Prime.not_isUnit`.
+Öffnen Sie `AlgebraInLean/Polynomials.lean` und ersetzen Sie das
+`sorry` durch einen Beweis.
+
+```lean
+theorem xn_sub_p_irreduzibel (n : ℕ) (hn : 0 < n) (p : ℕ)
+    (hp : p.Prime) :
+    Irreducible (X ^ n - C (p : ℤ)) := by
+  sorry
+```
diff --git a/README.md b/README.md
index b17de5a..790f99b 100644
--- a/README.md
+++ b/README.md
@@ -34,6 +34,8 @@ Lean/Mathlib.
 |------|---------------|-------|
 | `AlgebraInLean/Basics.lean` | Kapitel 2 | First steps: tactics, groups in Mathlib |
 | `AlgebraInLean/Quotients.lean` | Kapitel 2, 17 | Kernels, normal subgroups, quotient groups |
+| `AlgebraInLean/Ideals.lean` | Kapitel 9 | Ideals; ℤ is a principal ideal ring |
+| `AlgebraInLean/Polynomials.lean` | Kapitel 7 | Polynomials; Eisenstein's criterion applied |
 | `AlgebraInLean/LittleFermat.lean` | Kapitel 17 | Fermat's little theorem via Lagrange |
 | `AlgebraInLean/Cauchy.lean` | Kapitel 18 | The key lemma on fixed points and Cauchy's theorem |