Cleanup and final touches

2026-08-13 10:08:19 +02:00
1 parent 4ff2bb5fb2
commit cc75cdc801
@@ -61,8 +61,8 @@ das Inverse `a⁻¹`; die Axiome heißen `mul_assoc`, `one_mul`,

 Ein Unterschied fällt auf: Das Skript *fordert* die
 Eindeutigkeit von neutralem Element und Inversen, Mathlib
-nicht.  Das ist kein Widerspruch — die Eindeutigkeit folgt
-aus den übrigen Axiomen.  Genau das beweisen wir jetzt, mit
+nicht.  Das ist kein Widerspruch, denn die Eindeutigkeit
+folgt aus den übrigen Axiomen.  Genau das beweisen wir jetzt, mit
 dem Standardargument aus der linearen Algebra:

 *Es sei e ein weiteres Element, das von links neutral wirkt.
@@ -83,7 +83,7 @@ theorem neutral_eindeutig {G : Type*} [Group G] (e : G)
 Zeigen Sie ebenso die Eindeutigkeit des Inversen: Wenn
 a·b = 1 ist, dann ist b bereits *das* Inverse a⁻¹.  Das
 Standardargument: b = 1·b = (a⁻¹·a)·b = a⁻¹·(a·b) = a⁻¹·1
-= a⁻¹.  Ersetzen Sie das `sorry` durch einen Beweis — die
+= a⁻¹.  Ersetzen Sie das `sorry` durch einen Beweis.  Die
 Taktik `calc` aus dem Beweis oben und die Lemmata `one_mul`,
 `inv_mul_cancel`, `mul_assoc`, `mul_one` genügen.
 -/
@@ -33,8 +33,8 @@ Wie sagt Mathlib das alles?

 * „eine Gruppe der Ordnung p^m“: Dafür hat Mathlib ein
  Prädikat `IsPGroup p G` („die Ordnung jedes Elements ist
-  eine p-Potenz“ — für endliche Gruppen ist das äquivalent,
-  nach dem Satz von Cauchy unten!).  Das Lemma
+  eine p-Potenz“; für endliche Gruppen ist das nach dem Satz
+  von Cauchy unten äquivalent).  Das Lemma
  `IsPGroup.of_card` übersetzt unsere Voraussetzung
  `Nat.card G = p ^ m` dorthin.

@@ -48,7 +48,7 @@ Wie sagt Mathlib das alles?

 Der Beweis im Skript zerlegt M in Bahnen und zitiert die
 Bahnengleichung.  Genau so beweist Mathlib die Aussage
-`IsPGroup.card_modEq_card_fixedPoints` — wir zitieren hier
+`IsPGroup.card_modEq_card_fixedPoints`.  Wir zitieren hier
 also einfach die Bibliothek, so wie das Skript an dieser
 Stelle Satz 17.2.1 zitiert.
 -/
@@ -69,15 +69,15 @@ Ordnung p.*

 Wir folgen dem Beweis des Skripts Satz für Satz.  Der Beweis
 konstruiert eine raffinierte Hilfsmenge mit einer raffinierten
-Gruppenwirkung — diesmal gibt es also vor dem eigentlichen
+Gruppenwirkung.  Diesmal gibt es also vor dem eigentlichen
 Satz echte Arbeit: Wir bauen erst die Menge und die Wirkung.

 „Betrachte die Menge
 M = { (a₁, …, a_p) ∈ G ⨯ ⋯ ⨯ G : a₁·a₂ ⋯ a_p = e }.“

 Mathlib kennt diese Menge.  Ein p-Tupel von Gruppenelementen
-ist ein `List.Vector G p` — eine Liste der Länge p —, und M
-ist die Menge `Equiv.Perm.vectorsProdEqOne G p` aller
+ist ein `List.Vector G p`, also eine Liste der Länge p.  Und
+M ist die Menge `Equiv.Perm.vectorsProdEqOne G p` aller
 Vektoren, deren Einträge sich zu 1 multiplizieren.

 „Gegeben ein Tupel (a₁, …, a_p) ∈ M, dann stellen wir erst
@@ -98,8 +98,9 @@ Vertauschen wirken.“

 Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p`
 um k Stellen ist `VectorsProdEqOne.rotate v k`.  Die Fußnote
-des Skripts — der Shift bildet M auf sich ab, „weil in jeder
-Gruppe aus a·b = e auch b·a = e gilt“ — ist das Mathlib-Lemma
+des Skripts begründet, dass der Shift M auf sich abbildet,
+„weil in jeder Gruppe aus a·b = e auch b·a = e gilt“.  In
+Mathlib ist das das Lemma
 `List.prod_rotate_eq_one_of_prod_eq_one`, das schon in der
 Definition von `rotate` steckt.

@@ -109,7 +110,7 @@ Shift um j + k ist der Shift um k gefolgt vom Shift um j.
 Mathlib stellt `rotate_zero`, `rotate_rotate` und
 `rotate_length` bereit (der Shift um die volle Länge p tut
 nichts); daraus leiten wir zuerst ab, dass der Shift nur von
-der Verschiebung *modulo p* abhängt — genau deshalb wirkt
+der Verschiebung *modulo p* abhängt.  Genau deshalb wirkt
 ℤ/(p) und nicht bloß ℕ.
 -/

@@ -163,7 +164,7 @@ M₀ = { (a, …, a) ∈ G^p : a^p = e }.“

 Mit anderen Worten: Ein Tupel ist genau dann ein Fixpunkt,
 wenn es konstant ist, seine Liste also für ein a die Liste
-`List.replicate p a` — das ist (a, …, a) — ist.  (Die
+`List.replicate p a` = (a, …, a) ist.  (Die
 Bedingung a^p = e gilt dann automatisch, weil sich die
 Einträge eines Tupels in M zu e multiplizieren.)  Der
 Schlüsselschritt ist das Lemma
@@ -298,7 +299,7 @@ theorem cauchy {G : Type*} [Group G] [Fintype G] {p : ℕ}
   eine p-Potenz ist.  Dann ist das Zentrum von G nicht
   trivial.*  Beweisen Sie das in Lean: Wenden Sie
   `key_lemma` auf die Konjugationswirkung von G auf sich
-   selbst an — oder finden Sie die Aussage in Mathlib.
+   selbst an, oder finden Sie die Aussage in Mathlib.
   Ersetzen Sie dazu das `sorry` durch einen Beweis.
 -/

@@ -18,7 +18,7 @@ namespace AlgebraInLean
 ## Das Mathlib-Wörterbuch

 * Eine Körpererweiterung L/K ist in Mathlib eine
-  `Algebra K L`-Instanz zwischen zwei Körpern — L wird damit
+  `Algebra K L`-Instanz zwischen zwei Körpern.  Damit wird L
  insbesondere ein K-Vektorraum, genau wie im Skript.

 * Eine Kette K ⊆ L ⊆ M besteht aus drei Algebra-Instanzen
@@ -29,8 +29,8 @@ namespace AlgebraInLean
 * Der Grad [L:K] heißt `Module.finrank K L`.  Achtung, hier
  weicht die Konvention vom Skript ab: `finrank` hat Werte
  in ℕ, und unendlichdimensionale Erweiterungen bekommen
-  den Wert 0 — wo das Skript in seiner Fußnote mit ∞
-  rechnet, rechnet Mathlib mit 0.  „[L:K] ist endlich“ ist
+  den Wert 0.  Wo das Skript in seiner Fußnote mit ∞
+  rechnet, rechnet Mathlib also mit 0.  „[L:K] ist endlich“ ist
  die Typklasse `FiniteDimensional K L`.

 ## Die Gradformel
@@ -40,7 +40,7 @@ Satz 3.6.1 des Skripts, mit Beweis:
 „Es sei K ⊆ L ⊆ M eine Kette von Körpererweiterungen.  Dann
 gilt die Gleichung [M:K] = [M:L]·[L:K].“

-„Wir kümmern uns zuerst um die unendlichen Fälle …“ — diese
+„Wir kümmern uns zuerst um die unendlichen Fälle …“  Diese
 Fälle entfallen in unserer Fassung, weil wir Endlichkeit
 voraussetzen; in Mathlibs 0-Konvention gilt die Formel
 sogar uneingeschränkt (`Module.finrank_mul_finrank`).
@@ -51,9 +51,9 @@ m₁, …, m_b von M als L-Vektorraum.  Ich behaupte, dass die
 a·b Produkte (ℓᵢ·mⱼ) eine Basis von M als K-Vektorraum
 bilden; damit ist dann sofort [M:K] = a·b gezeigt.“

-Die Behauptung — mit den beiden Beweisschritten
+Die Behauptung zerfällt in die beiden Beweisschritte
 „Die Produkte bilden ein Erzeugendensystem“ und „Die
-Produkte sind linear unabhängig“ — ist in Mathlib die
+Produkte sind linear unabhängig“.  In Mathlib ist sie die
 Konstruktion `Basis.smulTower`: Aus einer Basis ℓ von L/K
 und einer Basis m von M/L baut sie die Basis (ℓᵢ • mⱼ) von
 M/K (das Lemma `Basis.smulTower_apply` bestätigt, dass die
@@ -85,7 +85,7 @@ theorem gradformel (K L M : Type*) [Field K] [Field L]
   von `Basis.smulTower`: Das „Einsetzen“ im
   Erzeugendensystem-Schritt und das „Umsortieren“ im
   Unabhängigkeits-Schritt werden dort durch die
-   Komposition der Koordinatenabbildungen erledigt —
+   Komposition der Koordinatenabbildungen erledigt.
   `smulTower_repr` sagt, dass die (i,j)-Koordinate von x
   gerade die i-te Koordinate der j-ten Koordinate ist:
   exakt das μᵢⱼ aus dem Skript.
@@ -101,8 +101,8 @@ Das erste Korollar des Skripts zur Gradformel: „Es sei
 K ⊆ L ⊆ M eine Kette von Körpererweiterungen.  Wenn [M:K]
 endlich ist, dann ist [L:K] endlich, und sogar ein Teiler
 von [M:K].“  Der erste Teil ist `Module.Finite.left` (und
-`Module.Finite.right` liefert die Endlichkeit von [M:L]) —
-beide müssen mit `have := …` in den Kontext geholt werden,
+`Module.Finite.right` liefert die Endlichkeit von [M:L]).
+Beide müssen mit `have := …` in den Kontext geholt werden,
 damit die Instanzsuche sie sieht.  Der Teiler-Teil ist die
 Übung: Ersetzen Sie das `sorry` durch einen Beweis mit
 `gradformel`.
@@ -25,7 +25,7 @@ open IntermediateField

 * Das Minimalpolynom heißt `minpoly K a`; der Grad [a:K] des
  Skripts ist `(minpoly K a).natDegree`.  Für transzendentes a
-  ist `minpoly K a = 0` — wieder die 0-Konvention für ∞.
+  ist `minpoly K a = 0`; das ist wieder die 0-Konvention für ∞.

 * Der Zwischenkörper K(a) heißt `K⟮a⟯`, kurz für
  `IntermediateField.adjoin K {a}`; die Notation kommt mit
@@ -39,8 +39,8 @@ open IntermediateField
 Satz 3.5.4 des Skripts: „Es sei L/K eine Körpererweiterung und
 es sei a ∈ L.  Dann gilt die Gleichheit [a:K] = [K(a):K].“

-Die Behauptung des Beweises — die Potenzen 1, a, …, a^{m-1}
-bilden eine Basis von K(a) — ist in Mathlib die Konstruktion
+Der Beweis behauptet, dass die Potenzen 1, a, …, a^{m-1} eine
+Basis von K(a) bilden.  In Mathlib ist das die Konstruktion
 `IntermediateField.adjoin.powerBasis`.
 -/

@@ -5,8 +5,9 @@ Algebra in Lean — Kapitel 14 des Skripts
 Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
 (Stefan Kebekus, CC-BY 4.0).  Sie übersetzt den Satz über
 den Frobenius-Endomorphismus
-(DefSatz_Frobenius-Endomorphismus) Satz für Satz nach Lean —
-den „Traum jedes Studienanfängers“: (a+b)^p = a^p + b^p.
+(DefSatz_Frobenius-Endomorphismus) Satz für Satz nach Lean.
+Es geht um den „Traum jedes Studienanfängers“:
+(a+b)^p = a^p + b^p.
 -/
 import Mathlib

@@ -101,17 +102,17 @@ theorem frobenius_add {R : Type*} [CommRing R] (p : ℕ)
   Ringmorphismus `frobenius R p : R →+* R`; die
   Additivität heißt dort `add_pow_char`.

-2. Die Beobachtung des Skripts — über einem Integritätsring
-   ist der Frobenius injektiv, über einem endlichen Körper
-   sogar bijektiv — führt zur Klassifikation endlicher
-   Körper: Zu jeder Primzahlpotenz p^n gibt es genau einen
+2. Das Skript beobachtet, dass der Frobenius über einem
+   Integritätsring injektiv und über einem endlichen Körper
+   sogar bijektiv ist.  Das führt zur Klassifikation
+   endlicher Körper: Zu jeder Primzahlpotenz p^n gibt es genau einen
   Körper mit p^n Elementen.  In Mathlib heißt er
   `GaloisField p n`.

 ## Übungsaufgabe

 Der Frobenius des Körpers 𝔽_p ist die Identität: Für jedes
-a ∈ 𝔽_p ist a^p = a.  Das ist ein alter Bekannter — der
+a ∈ 𝔽_p ist a^p = a.  Das ist ein alter Bekannter: der
 kleine Satz von Fermat aus unserem dritten Kapitel!  In
 Mathlib heißt er `ZMod.pow_card`.  Ersetzen Sie das `sorry`
 durch einen Beweis.
@@ -5,7 +5,7 @@ Algebra in Lean — Kapitel 15 und 16 des Skripts
 Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
 (Stefan Kebekus, CC-BY 4.0).  Sie zeigt, wie Mathlib die
 Begriffe der Galoistheorie darstellt, übersetzt die
-Fixkörper-Konstruktion (DefSatz_Fixkoerper) — und die
+Fixkörper-Konstruktion (DefSatz_Fixkoerper).  Die
 „Hausaufgabe“ des Skripts wird auch hier zur Übungsaufgabe.
 -/
 import Mathlib
@@ -21,7 +21,7 @@ namespace AlgebraInLean
  `L ≃ₐ[K] L` der K-Algebren-Automorphismen; Mathlib stellt
  dafür sogar die Notation `Gal(L/K)` bereit.

-* „L/K ist galoissch“ ist die Typklasse `IsGalois K L` —
+* „L/K ist galoissch“ ist die Typklasse `IsGalois K L`,
  definiert als „separabel und normal“, genau wie im
  Skript.

@@ -41,7 +41,7 @@ von L.  Der Beweis des folgenden Satzes ist eine
 Hausaufgabe.*

 Wir definieren die Menge in Lean und beweisen exemplarisch
-die Abgeschlossenheit unter der Multiplikation — der Rest
+die Abgeschlossenheit unter der Multiplikation.  Der Rest
 der Hausaufgabe ist, wie im Skript, Ihre Übungsaufgabe.
 -/

@@ -67,7 +67,7 @@ Mathlib; wir zitieren sie mit ihren Namen.
 Untergruppe der Automorphismengruppe eines Körpers L und es
 sei K := Fix G.  Dann ist L/K eine Galoiserweiterung mit
 Galoisgruppe Gal(L/K) = G.  Insbesondere ist [L:K] = |G|.*
-— Die Gradaussage ist `FixedPoints.finrank_eq_card`; das
+Die Gradaussage ist `FixedPoints.finrank_eq_card`; das
 gebündelte Fixkörper-Objekt heißt dort
 `FixedPoints.subfield G L`.

@@ -75,7 +75,7 @@ gebündelte Fixkörper-Objekt heißt dort
 Galoiserweiterung mit Galoisgruppe G.  Dann sind die
 Abbildungen Z ↦ Gal(L/Z) und H ↦ Fix H zueinander inverse,
 inklusionsumkehrende Bijektionen zwischen Zwischenkörpern
-und Untergruppen […].*  — In Mathlib ist das der
+und Untergruppen […].*  In Mathlib ist das der
 ordnungsumkehrende Isomorphismus
 `IsGalois.intermediateFieldEquivSubgroup`; das „ᵒᵈ“
 (order dual) im Typ ist genau das „inklusionsumkehrend“ des
@@ -94,8 +94,8 @@ example (K L : Type*) [Field K] [Field L] [Algebra K L]
 ## Übungsaufgabe

 Die „Hausaufgabe“ des Skripts: Vervollständigen Sie den
-Nachweis, dass Fix G ein Unterkörper ist — Abgeschlossenheit
-unter Addition und unter Inversen.  Für die Addition ist
+Nachweis, dass Fix G ein Unterkörper ist, also die
+Abgeschlossenheit unter Addition und unter Inversen.  Für die Addition ist
 `map_add` das Gegenstück zu `map_mul`; für das Inverse
 respektieren Körperautomorphismen auch die Division:
 `map_inv₀`.  Ersetzen Sie die beiden `sorry` durch Beweise.
@@ -4,8 +4,8 @@ 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.
+ein Hauptidealring“ (satz:9-1-4) Satz für Satz nach Lean.
+Es ist der klassische Beweis über Division mit Rest.
 -/
 import Mathlib

@@ -51,7 +51,7 @@ 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
+gleich beliebige b; die Division mit Rest in Lean
 funktioniert für alle ganzen Zahlen.
 -/

@@ -4,8 +4,8 @@ Algebra in Lean — Kapitel 17

 Diese Datei begleitet das Skript „Algebra und Zahlentheorie“
 (Stefan Kebekus, CC-BY 4.0).  Sie übersetzt einen Satz des
-Skripts — den kleinen Satz von Fermat, `satz:kleinerFermat` in
-Kapitel 17 — Satz für Satz nach Lean.  Das deutsche Original
+Skripts Satz für Satz nach Lean: den kleinen Satz von Fermat
+(`satz:kleinerFermat` in Kapitel 17).  Das deutsche Original
 jedes Beweissatzes steht als Kommentar direkt über dem
 Lean-Code, der ihn umsetzt: So sieht man, wie sich die
 Standardphrasen eines Vorlesungsbeweises nach Lean/Mathlib
@@ -26,7 +26,7 @@ Bevor wir das in Lean formulieren können, müssen wir wissen,
 wie Mathlib über die beteiligten Objekte spricht.

 * Der Restklassenring ℤ/(p) heißt `ZMod p`.  Die Restklasse
-  einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` —
+  einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)`;
  Lean fügt den kanonischen Ringmorphismus ℤ → ℤ/(p)
  automatisch ein („Koerzion“).

@@ -41,7 +41,7 @@ wie Mathlib über die beteiligten Objekte spricht.

 * Das Skript sagt „es sei p eine Primzahl“.  In Lean führen
  wir die Primalität von `p` als Hypothese `hp : p.Prime` mit.
-  Manche Tatsachen — etwa dass ℤ/(p) ein Körper ist — findet
+  Manche Tatsachen, etwa dass ℤ/(p) ein Körper ist, findet
  Leans Automatisierung nur, wenn die Hypothese als *Instanz*
  registriert ist; genau das leistet die erste Beweiszeile
  `have : Fact p.Prime := ⟨hp⟩`.
@@ -108,7 +108,7 @@ example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a :=
 2. **Übungsaufgabe** (das ist `bem:kleinerFermat` im Skript).
   In Anwendungen verwendet man häufig die äquivalente
   Formulierung a^(p−1) ≡ 1 (mod p) für nicht durch p
-   teilbare a.  Leiten Sie sie aus `little_fermat` ab — oder
+   teilbare a.  Leiten Sie sie aus `little_fermat` ab, oder
   geben Sie einen direkten Beweis nach den Ideen oben.
   Ersetzen Sie dazu das `sorry` durch einen Beweis.
 -/
@@ -25,7 +25,7 @@ open Polynomial
  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
+  Achtung: `degree` hat Werte in `WithBot ℕ`; das
  Nullpolynom bekommt den Grad ⊥ („minus unendlich“, wie im
  Skript).  Daneben gibt es `f.natDegree : ℕ`.

@@ -47,7 +47,7 @@ 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
+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
@@ -59,7 +59,7 @@ aus ggT = 1 folgt) verlangt Mathlib direkt
 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
+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.
@@ -84,7 +84,7 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
  · 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
+  -- Koeffizienten −r (bei k = 0) und 0 (sonst), beide
  -- durch p teilbar.
  · intro k hk
    have hkn : k < n := by
@@ -116,16 +116,16 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
   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.
+2. Das zweite Beispiel des Skripts greifen wir im Kapitel
+   über Körpererweiterungen wieder auf: xⁿ − p ist
+   irreduzibel und deshalb das Minimalpolynom von ⁿ√p.

 ## Ü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² ∤ 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
@@ -24,7 +24,7 @@ namespace AlgebraInLean
  Verknüpfung und Inversen abgeschlossen ist, sagen
  `U.mul_mem` und `U.inv_mem`.

-* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein
+* Ein Gruppenmorphismus ist ein Term `φ : G →* Q`, ein
  „Bündel“ aus der Abbildung und den Nachweisen
  `map_mul : φ (a·b) = φ a · φ b` (daraus folgen
  `map_one` und `map_inv`).  Der Kern heißt `φ.ker`;
@@ -64,7 +64,7 @@ Mathlib kennt diese Aussage als Instanz
 `MonoidHom.normal_ker : φ.ker.Normal`.  Das Skript fährt
 fort: Untergruppen mit dieser Eigenschaft heißen *normale
 Untergruppen* oder *Normalteiler*, und die Bedingung ist
-nicht nur notwendig, sondern auch hinreichend — zu jedem
+nicht nur notwendig, sondern auch hinreichend: Zu jedem
 Normalteiler existiert eine Restklassengruppe.

 ## Die Restklassengruppe und ihre universelle Eigenschaft
@@ -73,8 +73,8 @@ Das Skript definiert die Restklassengruppe in Kapitel 17.3
 über ihre universelle Eigenschaft.  Mathlib stellt beides
 bereit: den Quotienten `G ⧸ N` mit der Quotientenabbildung
 `QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle
-Eigenschaft als `QuotientGroup.lift` — gegeben ein
-Morphismus `α : G →* H` mit `N ≤ α.ker` erhält man den
+Eigenschaft als `QuotientGroup.lift`.  Gegeben ein
+Morphismus `α : G →* H` mit `N ≤ α.ker`, erhält man den
 induzierten Morphismus auf dem Quotienten:
 -/

@@ -126,7 +126,7 @@ theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
 ## Übungsaufgabe

 Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit
-unter der Verknüpfung zu zeigen — prüfen Sie den
+unter der Verknüpfung zu zeigen.  Prüfen Sie den
 verschwiegenen Teil selbst nach: U·N ist auch abgeschlossen
 unter Inversen.  Tipp: (u·n)⁻¹ = u⁻¹·(u·n⁻¹·u⁻¹), und der
 zweite Faktor liegt nach `conj_mem` in N.  Ersetzen Sie das
@@ -23,9 +23,9 @@ namespace AlgebraInLean
  `IsSquare (a : ZMod p)`.

 * Das Lean-Lernthema dieses Kapitels ist die Taktik
-  `decide`: Aussagen über konkrete endliche Objekte —
-  „ist 7 ein Quadrat in 𝔽₁₇?“ — sind *entscheidbar*, und
-  Lean darf die Antwort einfach ausrechnen.  Das Ergebnis
+  `decide`: Aussagen über konkrete endliche Objekte sind
+  *entscheidbar*, etwa „ist 7 ein Quadrat in 𝔽₁₇?“.  Lean
+  darf die Antwort also einfach ausrechnen.  Das Ergebnis
  ist ein vollwertiger Beweis.

 ## Das Reziprozitätsgesetz
@@ -37,11 +37,12 @@ und q zwei unterschiedliche, ungerade Primzahlen.  Dann
 gilt die Gleichung
 (p/q)·(q/p) = (−1)^((p−1)/2 · (q−1)/2).*

-In Mathlib: `legendreSym.quadratic_reciprocity` — dort mit
-den Exponenten `p / 2` geschrieben, was für ungerade p
-dasselbe ist wie (p−1)/2.  Dazu die beiden Ergänzungssätze:
-Der erste — (−1/p) = 1 genau für p ≡ 1 (mod 4) — ist in der
-Quadrat-Formulierung `ZMod.exists_sq_eq_neg_one_iff`:
+In Mathlib heißt der Satz `legendreSym.quadratic_reciprocity`.
+Dort stehen die Exponenten als `p / 2`, was für ungerade p
+dasselbe ist wie (p−1)/2.  Dazu kommen die beiden
+Ergänzungssätze.  Der erste besagt, dass (−1/p) = 1 genau für
+p ≡ 1 (mod 4) gilt; in der Quadrat-Formulierung ist er
+`ZMod.exists_sq_eq_neg_one_iff`:
 -/

 example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
@@ -86,8 +87,8 @@ von Fermat bewiesen haben.

 Ist 3 ein quadratischer Rest modulo 41?  Rechnen Sie erst
 von Hand nach dem Muster des Skript-Beispiels (mit
-Reziprozität und den Ergänzungssätzen) — und lassen Sie
-dann Lean Ihre Antwort bestätigen.  Ersetzen Sie dazu das
+Reziprozität und den Ergänzungssätzen).  Lassen Sie dann
+Lean Ihre Antwort bestätigen.  Ersetzen Sie dazu das
 `sorry` durch einen Beweis.
 -/

@@ -19,10 +19,10 @@ 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
+Der Kern des Skript-Beweises ist in Mathlib das Lemma
+`isIntegral_trans`: adjungiere die endlich vielen Koeffizienten
+des Minimalpolynoms, schließe auf Endlichkeit und klettere mit
+der Gradformel den Turm hinauf.  Das Mathlib-Wörterbuch aus
 `AlgebraInLean/Elements.lean` gilt unverändert weiter.
 -/

@@ -14,6 +14,7 @@ import Book.Cauchy
 import Book.Frobenius
 import Book.Galois
 import Book.Reciprocity
+import Book.Appendix

 open Verso.Genre Manual

@@ -87,3 +88,5 @@ oder der ausführlichen Anleitung am Anfang der
 {include 0 Book.Galois}

 {include 0 Book.Reciprocity}
+
+{include 0 Book.Appendix}
@@ -0,0 +1,54 @@
+import VersoManual
+import Manual.Meta
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing true
+
+open Verso.Genre
+open Verso.Genre.Manual.InlineLean
+
+#doc (Manual) "Anhang: Lizenz und Hinweise" =>
+%%%
+htmlSplit := .never
+tag := "anhang"
+file := "anhang"
+%%%
+
+Dieser Anhang sagt, unter welchen Bedingungen Sie diese Notizen
+weiterverwenden dürfen, und wie sie entstanden sind.
+
+# Lizenz
+
+Diese Kursnotizen stehen, genau wie das begleitende Skript _Algebra
+und Zahlentheorie_, unter der Lizenz
+[Creative Commons Namensnennung 4.0 International (CC BY 4.0)](https://creativecommons.org/licenses/by/4.0/deed.de).
+
+Sie dürfen das Material also in jedem Format teilen und bearbeiten,
+auch kommerziell, solange Sie angemessene Urheber- und Rechteangaben
+machen, einen Link auf die Lizenz beifügen und angeben, ob Änderungen
+vorgenommen wurden.  Der vollständige Lizenztext liegt im Repository
+in der Datei `LICENSE`.
+
+Der zitierte Lean-Code lebt von [Mathlib](https://github.com/leanprover-community/mathlib4),
+das seinerseits unter der Apache-Lizenz 2.0 steht.  Die Namen der
+zitierten Lemmata und Definitionen gehören dorthin, nicht hierher.
+
+# Zur Entstehung: KI-Einsatz und Originalität
+
+Diese Notizen sind unter starkem Einsatz von KI-Werkzeugen (großen
+Sprachmodellen) entstanden.  Das gilt für die Lean-Beweise ebenso wie
+für die deutsche Prosa: Beides wurde weitgehend maschinell entworfen
+und von mir anschließend geprüft, korrigiert und überarbeitet.
+
+Ich erhebe daher *keinerlei Anspruch auf Originalität*.  Die
+Mathematik stammt aus der Vorlesung und ist Standardstoff; die
+Beweisideen stammen aus dem Skript; die eigentliche Arbeit im Beweis
+leisten die Lemmata aus Mathlib, die hier nur zusammengesetzt und
+kommentiert werden.  Der Beitrag dieser Notizen liegt allein in der
+Auswahl und der Aufbereitung des Materials.
+
+Ein Trost bleibt: Sämtlicher Lean-Code in diesen Notizen wird beim
+Bauen des Buches mitelaboriert.  Die gezeigten Beweise sind also vom
+Compiler geprüft, ganz gleich, wer oder was sie geschrieben hat.  Für
+die Prosa gilt das nicht — Fehler darin gehen zu meinen Lasten.
+Hinweise darauf nehme ich gerne entgegen.
@@ -64,7 +64,8 @@ die Axiome heißen `mul_assoc`, `one_mul`, `mul_one`,

 Ein Unterschied fällt auf: Das Skript _fordert_ die Eindeutigkeit von
 neutralem Element und Inversen, Mathlib nicht.  Das ist kein
-Widerspruch — die Eindeutigkeit folgt aus den übrigen Axiomen.  Genau
+Widerspruch, denn die Eindeutigkeit folgt aus den übrigen Axiomen.
+Genau
 das beweisen wir jetzt, mit dem Standardargument aus der linearen
 Algebra:

@@ -74,8 +75,8 @@ Algebra:
  $`e = e \cdot 1 = 1`.

 Der Lean-Beweis benutzt die Taktik `calc`, die eine Kette von
-Gleichungen Schritt für Schritt abarbeitet — das Lean-Gegenstück zur
-Gleichungskette am Ende des Textbeweises:
+Gleichungen Schritt für Schritt abarbeitet; sie ist das
+Lean-Gegenstück zur Gleichungskette am Ende des Textbeweises:

 ```lean
 theorem neutral_eindeutig {G : Type*} [Group G] (e : G)
@@ -96,7 +97,7 @@ $$`b = 1 \cdot b = (a^{-1} \cdot a) \cdot b = a^{-1} \cdot (a \cdot b) = a^{-1}

 Öffnen Sie
 `AlgebraInLean/Basics.lean` und ersetzen Sie das `sorry` durch einen
-Beweis — `calc` und die Lemmata `one_mul`, `inv_mul_cancel`,
+Beweis.  `calc` und die Lemmata `one_mul`, `inv_mul_cancel`,
 `mul_assoc`, `mul_one` genügen.

 ```lean
@@ -40,8 +40,8 @@ Wie sagt Mathlib das alles?

 * „eine Gruppe der Ordnung $`p^m`“: Dafür hat Mathlib ein Prädikat
  `IsPGroup p G` („die Ordnung jedes Elements ist eine
-  $`p`-Potenz“ — für endliche Gruppen ist das äquivalent, nach dem
-  Satz von Cauchy unten!).  Das Lemma `IsPGroup.of_card` übersetzt
+  $`p`-Potenz“; für endliche Gruppen ist das nach dem Satz von
+  Cauchy unten äquivalent).  Das Lemma `IsPGroup.of_card` übersetzt
  unsere Voraussetzung `Nat.card G = p ^ m` dorthin.

 * „die auf einer endlichen Menge $`M` operiert“: Eine Wirkung von
@@ -54,7 +54,7 @@ Wie sagt Mathlib das alles?

 Der Beweis im Skript zerlegt $`M` in Bahnen und zitiert die
 Bahnengleichung.  Genau so beweist Mathlib die Aussage
-`IsPGroup.card_modEq_card_fixedPoints` — wir zitieren hier also
+`IsPGroup.card_modEq_card_fixedPoints`.  Wir zitieren hier also
 einfach die Bibliothek, so wie das Skript an dieser Stelle Satz 17.2.1
 zitiert.

@@ -82,7 +82,7 @@ gleich auf.)

 Wir folgen dem Beweis des Skripts Satz für Satz.  Der Beweis
 konstruiert eine raffinierte Hilfsmenge mit einer raffinierten
-Gruppenwirkung — diesmal gibt es also vor dem eigentlichen Satz echte
+Gruppenwirkung.  Diesmal gibt es also vor dem eigentlichen Satz echte
 Arbeit: Wir bauen erst die Menge und die Wirkung.

 ## Die Menge M
@@ -91,8 +91,8 @@ Arbeit: Wir bauen erst die Menge und die Wirkung.
 $`M = \bigl\{ (a_1, \dots, a_p) \in G \times \dots \times G : a_1 \cdot a_2 \cdots a_p = e \bigr\}`.“

 Mathlib kennt diese Menge.  Ein $`p`-Tupel von Gruppenelementen ist
-ein `List.Vector G p` — eine Liste der Länge $`p` —, und $`M` ist die
-Menge `Equiv.Perm.vectorsProdEqOne G p` aller Vektoren, deren
+ein `List.Vector G p`, also eine Liste der Länge $`p`.  Und $`M` ist
+die Menge `Equiv.Perm.vectorsProdEqOne G p` aller Vektoren, deren
 Einträge sich zu 1 multiplizieren.

 „Gegeben ein Tupel $`(a_1, \dots, a_p) \in M`, dann stellen wir erst
@@ -120,9 +120,9 @@ Vertauschen wirken.“

 Der zyklische Shift eines Vektors `v ∈ vectorsProdEqOne G p` um
 $`k` Stellen ist `VectorsProdEqOne.rotate v k`.  Die Fußnote des
-Skripts — der Shift bildet $`M` auf sich ab, „weil in jeder Gruppe
-aus $`a \cdot b = e` auch $`b \cdot a = e` gilt“ — ist das
-Mathlib-Lemma
+Skripts begründet, dass der Shift $`M` auf sich abbildet, „weil in
+jeder Gruppe aus $`a \cdot b = e` auch $`b \cdot a = e` gilt“.  In
+Mathlib ist das das Lemma
 `List.prod_rotate_eq_one_of_prod_eq_one`, das schon in der Definition
 von `rotate` steckt.

@@ -131,8 +131,8 @@ Wirkungsaxiome nachprüfen: Der Shift um 0 tut nichts, und der Shift
 um $`j + k` ist der Shift um $`k` gefolgt vom Shift um $`j`.  Mathlib
 stellt `rotate_zero`, `rotate_rotate` und `rotate_length` bereit (der
 Shift um die volle Länge $`p` tut nichts); daraus leiten wir zuerst
-ab, dass der Shift nur von der Verschiebung _modulo p_ abhängt —
-genau deshalb wirkt $`\mathbb{Z}/(p)` und nicht bloß
+ab, dass der Shift nur von der Verschiebung _modulo p_ abhängt.
+Genau deshalb wirkt $`\mathbb{Z}/(p)` und nicht bloß
 $`\mathbb{N}`.

 ```lean
@@ -186,7 +186,7 @@ $`M_0 = \{ (a, \dots, a) \in G^p : a^p = e \}`.“

 Mit anderen Worten: Ein Tupel ist genau dann ein Fixpunkt, wenn es
 konstant ist, seine Liste also für ein $`a` die Liste
-`List.replicate p a` — das ist $`(a, \dots, a)` — ist.  (Die
+`List.replicate p a` = $`(a, \dots, a)` ist.  (Die
 Bedingung $`a^p = e` gilt dann automatisch, weil sich die Einträge
 eines Tupels in $`M` zu $`e` multiplizieren.)  Der Schlüsselschritt ist das Lemma
 `List.rotate_one_eq_self_iff_eq_replicate`: Eine Liste, die der
@@ -322,7 +322,7 @@ Das ist Satz 18.2.3 im Skript: _Es sei $`p` eine Primzahl und $`G`
 eine nichttriviale Gruppe, deren Ordnung eine $`p`-Potenz ist.  Dann
 ist das Zentrum von $`G` nicht trivial._  Beweisen Sie das in Lean:
 Wenden Sie `key_lemma` auf die Konjugationswirkung von $`G` auf sich
-selbst an —
+selbst an,
 oder finden Sie die Aussage in Mathlib.  Öffnen Sie
 `AlgebraInLean/Cauchy.lean` im Übungs-Repository und ersetzen Sie das
 `sorry` durch einen Beweis.
@@ -28,7 +28,7 @@ und Körpererweiterungen als Vektorräume.
 # Das Mathlib-Wörterbuch

 * Eine Körpererweiterung $`L/K` ist in Mathlib eine
-  `Algebra K L`-Instanz zwischen zwei Körpern — $`L` wird damit
+  `Algebra K L`-Instanz zwischen zwei Körpern.  Damit wird $`L`
  insbesondere ein $`K`-Vektorraum, genau wie im Skript.

 * Eine Kette $`K \subseteq L \subseteq M` besteht aus drei
@@ -38,9 +38,9 @@ und Körpererweiterungen als Vektorräume.

 * Der Grad $`[L:K]` heißt `Module.finrank K L`.  Achtung, hier weicht
  die Konvention vom Skript ab: `finrank` hat Werte in $`\mathbb{N}`,
-  und unendlichdimensionale Erweiterungen bekommen den Wert 0 — wo
+  und unendlichdimensionale Erweiterungen bekommen den Wert 0.  Wo
  das Skript in seiner Fußnote mit $`\infty` rechnet, rechnet Mathlib
-  mit 0.  „$`[L:K]` ist endlich“ ist die Typklasse
+  also mit 0.  „$`[L:K]` ist endlich“ ist die Typklasse
  `FiniteDimensional K L`.

 # Die Gradformel
@@ -63,9 +63,10 @@ Die unendlichen Fälle entfallen in unserer Fassung, weil wir
 Endlichkeit voraussetzen; in Mathlibs 0-Konvention gilt die Formel
 sogar uneingeschränkt (`Module.finrank_mul_finrank`).

-Die Behauptung — mit den beiden Beweisschritten „Die Produkte bilden
-ein Erzeugendensystem“ und „Die Produkte sind linear unabhängig“ —
-ist in Mathlib die Konstruktion `Basis.smulTower`: Aus einer Basis
+Die Behauptung zerfällt in die beiden Beweisschritte „Die Produkte
+bilden ein Erzeugendensystem“ und „Die Produkte sind linear
+unabhängig“.  In Mathlib ist sie die Konstruktion
+`Basis.smulTower`: Aus einer Basis
 $`\ell` von $`L/K` und einer Basis $`m` von $`M/L` baut sie die
 Basis $`(\ell_i \cdot m_j)` von $`M/K` (das Lemma
 `Basis.smulTower_apply` bestätigt,
@@ -98,7 +99,7 @@ theorem gradformel (K L M : Type*) [Field K] [Field L]
 Die beiden Beweisschritte des Skripts stecken im Beweis von
 `Basis.smulTower`: Das „Einsetzen“ im Erzeugendensystem-Schritt und
 das „Umsortieren“ im Unabhängigkeits-Schritt werden dort durch die
-Komposition der Koordinatenabbildungen erledigt —
+Komposition der Koordinatenabbildungen erledigt.
 `Basis.smulTower_repr` sagt, dass die $`(i,j)`-Koordinate von `x`
 gerade die $`i`-te Koordinate der $`j`-ten Koordinate ist: exakt das
 $`μ_{ij}` aus dem Skript.
@@ -112,7 +113,7 @@ Das erste Korollar des Skripts zur Gradformel:
  $`[L:K]` endlich, und sogar ein Teiler von $`[M:K]`.

 Der erste Teil ist `Module.Finite.left` (und `Module.Finite.right`
-liefert die Endlichkeit von $`[M:L]`) — beide müssen mit `have := …`
+liefert die Endlichkeit von $`[M:L]`).  Beide müssen mit `have := …`
 in den Kontext geholt werden, damit die Instanzsuche sie sieht.  Der
 Teiler-Teil ist die Übung: Öffnen Sie `AlgebraInLean/Degrees.lean`
 und ersetzen Sie das `sorry` durch einen Beweis mit `gradformel`.
@@ -127,9 +128,9 @@ theorem grad_teilt (K L M : Type*) [Field K] [Field L]

 # Der vollständige Beweis

-Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit —
-die Behauptung über die Produkte — haben wir bei `Basis.smulTower`
-eingekauft.  Zum Abschluss führen wir den Skript-Beweis selbst aus,
+Der Beweis oben ist ehrlich, aber kurz: Die eigentliche Arbeit haben
+wir bei `Basis.smulTower` eingekauft, nämlich die Behauptung über die
+Produkte.  Zum Abschluss führen wir den Skript-Beweis selbst aus,
 Satz für Satz.  Die unendlichen Fälle entfallen wie zuvor, weil wir
 Endlichkeit voraussetzen.

@@ -151,7 +152,7 @@ Der erste Schritt des Skripts:
  liefert $`m = \sum_{i,j} μ_{ij} \cdot (\ell_i \cdot m_j)`.

 In Lean heißen die Koeffizienten $`λ_j` und $`μ_{ij}` gerade
-`m.repr x j` und `ℓ.repr (m.repr x j) i` — das „Schreibe … als
+`m.repr x j` und `ℓ.repr (m.repr x j) i`.  Das „Schreibe … als
 Linearkombination“ des Skripts ist das Lemma `Basis.sum_repr`.  Das
 „Einsetzen“ ist eine kleine Rechnung mit dem Distributivgesetz
 `Finset.sum_smul` und der Turmbedingung `smul_assoc`,
@@ -203,7 +204,7 @@ Der zweite Schritt:

 Das Lemma `Fintype.linearIndependent_iff` übersetzt „linear
 unabhängig“ in genau die Sprechweise des Skripts: Jede Relation hat
-verschwindende Koeffizienten.  Wir benutzen es dreimal — einmal in
+verschwindende Koeffizienten.  Wir benutzen es dreimal: einmal in
 jede Richtung für die Basen `m` und `ℓ`, und einmal für die zu
 beweisende Aussage selbst.

@@ -252,8 +253,8 @@ Zum Schluss der Zusammenbau, wie im Skript angekündigt:
  als $`K`-Vektorraum bilden; damit ist dann sofort
  $`[M:K] = a \cdot b` gezeigt.

-Die Konstruktion `Module.Basis.mk` baut aus unseren beiden Lemmata —
-linear unabhängig und erzeugend — eine Basis; das „sofort gezeigt“
+Aus unseren beiden Lemmata (linear unabhängig, erzeugend) baut die
+Konstruktion `Module.Basis.mk` eine Basis.  Das „sofort gezeigt“
 ist wieder das Abzählen der Indexmenge `Fin a × Fin b`.

 ```lean
@@ -31,15 +31,15 @@ Kapitel, die Transitivität der Algebraizität.

 * „$`a` ist algebraisch über $`K`“ heißt `IsAlgebraic K a`.  Über
  Körpern ist das gleichbedeutend damit, dass $`a` Nullstelle
-  eines _normierten_ Polynoms ist — in Mathlib `IsIntegral K a`
-  („$`a` ist ganz über $`K`“).  Die Umrechnungen heißen
+  eines _normierten_ Polynoms ist; in Mathlib heißt das
+  `IsIntegral K a` („$`a` ist ganz über $`K`“).  Die Umrechnungen heißen
  `IsAlgebraic.isIntegral` und `IsIntegral.isAlgebraic`; die
  meisten Mathlib-Lemmata sind für `IsIntegral` formuliert.

 * Das Minimalpolynom heißt `minpoly K a`; der Grad $`[a:K]` des
  Skripts ist sein Grad `(minpoly K a).natDegree`.  Für
  transzendentes $`a` setzt Mathlib `minpoly K a = 0`, und das
-  Nullpolynom hat `natDegree` 0 — wir treffen also wieder die
+  Nullpolynom hat `natDegree` 0.  Damit treffen wir wieder die
  0-Konvention für $`\infty` aus dem letzten Kapitel.

 * Der Zwischenkörper $`K(a)` heißt `K⟮a⟯`, kurz für
@@ -47,9 +47,9 @@ Kapitel, die Transitivität der Algebraizität.
  durch `open IntermediateField` verfügbar; Vorsicht, `⟮…⟯` sind
  eigene Unicode-Zeichen, keine gewöhnlichen Klammern.

-* „Die Erweiterung $`L/K` ist algebraisch“ — jedes Element von
-  $`L` ist algebraisch über $`K` — ist die Typklasse
-  `Algebra.IsAlgebraic K L`.  Das elementweise Ausbuchstabieren
+* „Die Erweiterung $`L/K` ist algebraisch“ ist die Typklasse
+  `Algebra.IsAlgebraic K L`; gemeint ist, dass jedes Element von
+  $`L` algebraisch über $`K` ist.  Das elementweise Ausbuchstabieren
  übernimmt `Algebra.IsAlgebraic.isAlgebraic`.

 # Satz 3.5.4
@@ -73,14 +73,14 @@ Der Beweis im algebraischen Fall:
  Ich behaupte, dass $`V = K(a)` ist; damit ist dann
  $`[K(a):K] = \dim_K V = m` und der Satz ist bewiesen.  …

-Die Behauptung — mit den beiden Beweisschritten
+Die Behauptung zerfällt in die beiden Beweisschritte
 „Abgeschlossenheit unter Multiplikation“ und „Abgeschlossenheit
-unter Inversenbildung“ — ist in Mathlib die Konstruktion
+unter Inversenbildung“.  In Mathlib ist sie 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 — und wie dort holen wir den vollständigen
-Beweis am Ende des Kapitels nach.
+das Abzählen der Basis; den vollständigen Beweis holen wir wie
+dort am Ende des Kapitels nach.

 ```lean
 open IntermediateField
@@ -99,8 +99,8 @@ theorem grad_element {K L : Type*} [Field K] [Field L]
  rfl
 ```

-Den transzendenten Fall — $`[a:K] = ∞ = [K(a):K]` — behandelt
-das Skript mit den unendlichen Potenzen $`1, a, a^2, …`; in
+Im transzendenten Fall gilt $`[a:K] = ∞ = [K(a):K]`.  Das Skript
+behandelt ihn mit den unendlichen Potenzen $`1, a, a^2, …`; in
 Mathlibs 0-Konvention steht auf beiden Seiten schlicht 0.  Als
 fertiges Zitat heißt unser Satz übrigens
 `IntermediateField.adjoin.finrank`.
@@ -132,9 +132,9 @@ theorem einfach_algebraisch {K L : Type*} [Field K]

 # Der vollständige Beweis

-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
+Oben haben wir die eigentliche Arbeit bei
+`IntermediateField.adjoin.powerBasis` eingekauft: dass die Potenzen
+eine Basis von $`K(a)` bilden.  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,
@@ -159,7 +159,7 @@ noncomputable def potenzraum (K : Type*) {L : Type*}
    fun i : Fin (minpoly K a).natDegree => a ^ (i : ℕ))
 ```

-Ein Argument benutzt das Skript zweimal — einmal für $`a`, später
+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
@@ -21,8 +21,8 @@ file := "frobenius"
 %%%

 Dieses Kapitel übersetzt den Satz über den Frobenius-Endomorphismus
-aus Kapitel 14 des Skripts Satz für Satz nach Lean — den „Traum jedes
-Studienanfängers“: $`(a+b)^p = a^p + b^p`.
+aus Kapitel 14 des Skripts Satz für Satz nach Lean.  Es geht um den
+„Traum jedes Studienanfängers“: $`(a+b)^p = a^p + b^p`.

 # Das Mathlib-Wörterbuch

@@ -110,9 +110,9 @@ theorem frobenius_add {R : Type*} [CommRing R] (p : ℕ)

 Mathlib bündelt die drei Verträglichkeiten zum Ringmorphismus
 `frobenius R p : R →+* R`; die Additivität heißt dort
-`add_pow_char`.  Die Beobachtung des Skripts — über einem
-Integritätsring ist der Frobenius injektiv, über einem endlichen
-Körper sogar bijektiv — führt zur Klassifikation endlicher Körper:
+`add_pow_char`.  Das Skript beobachtet, dass der Frobenius über einem
+Integritätsring injektiv und über einem endlichen Körper sogar
+bijektiv ist.  Das führt zur Klassifikation endlicher Körper:
 Zu jeder Primzahlpotenz $`p^n` gibt es genau einen Körper mit
 $`p^n` Elementen.  In Mathlib heißt er `GaloisField p n`.

@@ -120,7 +120,7 @@ $`p^n` Elementen.  In Mathlib heißt er `GaloisField p n`.

 Der Frobenius des Körpers $`\mathbb{F}_p` ist die Identität: Für
 jedes $`a \in \mathbb{F}_p` ist $`a^p = a`.  Das ist ein alter
-Bekannter — der kleine
+Bekannter: der kleine
 Satz von Fermat aus unserem dritten Kapitel!  In Mathlib heißt er
 `ZMod.pow_card`.  Öffnen Sie `AlgebraInLean/Frobenius.lean` und
 ersetzen Sie das `sorry` durch einen Beweis.
@@ -23,8 +23,8 @@ file := "galois"

 Dieses Kapitel zeigt, wie Mathlib die Begriffe der Galoistheorie aus
 den Kapiteln 15 und 16 des Skripts darstellt, und übersetzt die
-Fixkörper-Konstruktion — deren Beweis im Skript eine „Hausaufgabe“
-ist und es auch hier bleibt.
+Fixkörper-Konstruktion.  Deren Beweis ist im Skript eine
+„Hausaufgabe“ und bleibt es auch hier.

 # Das Mathlib-Wörterbuch

@@ -32,7 +32,7 @@ ist und es auch hier bleibt.
  `L ≃ₐ[K] L` der K-Algebren-Automorphismen; Mathlib stellt dafür
  sogar die Notation `Gal(L/K)` bereit.

-* „$`L/K` ist galoissch“ ist die Typklasse `IsGalois K L` — definiert
+* „$`L/K` ist galoissch“ ist die Typklasse `IsGalois K L`, definiert
  als „separabel und normal“, genau wie im Skript.

 * Ein Zwischenkörper ist ein Term `Z : IntermediateField K L`; der
@@ -51,7 +51,7 @@ Satz und Definition 16.1.1 des Skripts:
  eine Hausaufgabe.

 Wir definieren die Menge in Lean und beweisen exemplarisch die
-Abgeschlossenheit unter der Multiplikation — der Rest der Hausaufgabe
+Abgeschlossenheit unter der Multiplikation.  Der Rest der Hausaufgabe
 ist, wie im Skript, Ihre Übungsaufgabe.

 ```lean
@@ -107,8 +107,8 @@ example (K L : Type*) [Field K] [Field L] [Algebra K L]
 # Übungsaufgabe

 Die „Hausaufgabe“ des Skripts: Vervollständigen Sie den Nachweis,
-dass `Fix G` ein Unterkörper ist — Abgeschlossenheit unter Addition
-und unter Inversen.  Für die Addition ist `map_add` das Gegenstück zu
+dass `Fix G` ein Unterkörper ist, also die Abgeschlossenheit unter
+Addition und unter Inversen.  Für die Addition ist `map_add` das Gegenstück zu
 `map_mul`; für das Inverse respektieren Körperautomorphismen auch die
 Division: `map_inv₀`.  Öffnen Sie `AlgebraInLean/Galois.lean` und
 ersetzen Sie die beiden `sorry` durch Beweise.
@@ -22,9 +22,9 @@ file := "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.
+Kapitel 9 des Skripts.  Es ist der klassische Beweis über Division
+mit Rest und zugleich unsere erste Begegnung mit dem
+Wohlordnungsprinzip in Lean.

 # Das Mathlib-Wörterbuch

@@ -62,7 +62,7 @@ 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
+beliebige $`b`; die Division mit Rest in Lean funktioniert für alle
 ganzen Zahlen.

 ```lean
@@ -36,9 +36,9 @@ deutsche Original, Aussage und Beweis:
  $`\overline{a}^{p-1} = 1 \in \mathbb{F}_p^*`, oder äquivalent
  $`a^p \equiv a \pmod{p}`. ∎

-Fünf Sätze.  Unser Ziel ist ein Lean-Beweis mit genau dieser Struktur —
-jeder deutsche Satz kehrt als Kommentar über dem Lean-Code wieder, der
-ihn umsetzt.
+Fünf Sätze.  Unser Ziel ist ein Lean-Beweis mit genau dieser
+Struktur: Jeder deutsche Satz kehrt als Kommentar über dem Lean-Code
+wieder, der ihn umsetzt.

 # Das Mathlib-Wörterbuch

@@ -46,7 +46,7 @@ Bevor wir den Satz überhaupt formulieren können, müssen wir wissen, wie
 Mathlib über die beteiligten Objekte spricht.

 * Der Restklassenring $`\mathbb{Z}/(p)` heißt `ZMod p`.  Die
-  Restklasse einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)` —
+  Restklasse einer ganzen Zahl `a : ℤ` schreibt sich `(a : ZMod p)`;
  Lean fügt den kanonischen Ringmorphismus
  $`\mathbb{Z} \to \mathbb{Z}/(p)` automatisch ein (eine _Koerzion_).

@@ -60,7 +60,7 @@ Mathlib über die beteiligten Objekte spricht.

 * Das Skript sagt „es sei $`p` eine Primzahl“.  In Lean führen wir die
  Primalität von `p` als Hypothese `hp : p.Prime` mit.  Manche
-  Tatsachen — etwa dass $`\mathbb{Z}/(p)` ein Körper ist — findet
+  Tatsachen, etwa dass $`\mathbb{Z}/(p)` ein Körper ist, findet
  Leans Automatisierung nur, wenn die Hypothese als _Instanz_
  registriert ist; genau das leistet die erste Beweiszeile
  `have : Fact p.Prime := ⟨hp⟩`.
@@ -141,7 +141,7 @@ example (p : ℕ) [Fact p.Prime] (a : ZMod p) : a ^ p = a :=
 Das ist die Bemerkung nach dem Satz im Skript: In Anwendungen
 verwendet man häufig die äquivalente Formulierung
 $`a^{p-1} \equiv 1 \pmod{p}` für nicht durch $`p` teilbare $`a`.  Leiten Sie
-sie aus `little_fermat` ab — oder geben Sie einen direkten Beweis nach
+sie aus `little_fermat` ab, oder geben Sie einen direkten Beweis nach
 den Ideen oben.  Öffnen Sie `AlgebraInLean/LittleFermat.lean` im
 Übungs-Repository und ersetzen Sie das `sorry` durch einen Beweis.

@@ -31,7 +31,7 @@ Polynom-API kennen.
  `X ^ 3 - C 2`.

 * Der k-te Koeffizient ist `f.coeff k`, der Grad `f.degree`.
-  Achtung: `degree` hat Werte in `WithBot ℕ` — das Nullpolynom
+  Achtung: `degree` hat Werte in `WithBot ℕ`; das Nullpolynom
  bekommt den Grad `⊥` („minus unendlich“, wie im Skript).  Daneben
  gibt es `f.natDegree : ℕ`.

@@ -55,7 +55,7 @@ Satz 7.2.1 des Skripts:

 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
+ein Primideal `P` statt eines Primelements $`p` formuliert.  Für uns
 ist `P` das Hauptideal $`(p)` aus dem letzten Kapitel, und „$`p`
 teilt $`a_k`“ wird zu `f.coeff k ∈ Ideal.span {p}`.  Statt
 „$`p \nmid a_n`“ (was im Skript aus $`\operatorname{ggT} = 1` folgt)
@@ -68,7 +68,7 @@ verlangt Mathlib direkt `f.leadingCoeff ∉ P`.
  ist.

 Das Skript lässt die Kontrolle der Eisenstein-Bedingungen als
-Kopfrechnung weg — in Lean führen wir sie aus und lernen dabei die
+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^n - r`, nämlich $`a_n = 1`,
 $`a_0 = -r` und $`a_k = 0` sonst.
@@ -95,7 +95,7 @@ theorem xn_sub_r_irreduzibel (n : ℕ) (hn : 0 < n) (r : ℤ)
  · 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
+  -- Koeffizienten −r (bei k = 0) und 0 (sonst), beide
  -- durch p teilbar.
  · intro k hk
    have hkn : k < n := by
@@ -125,9 +125,9 @@ 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^n - p` ist irreduzibel und deshalb
-das Minimalpolynom von $`\sqrt[n]{p}` — greifen wir im Kapitel über
-Körpererweiterungen wieder auf.
+zweite Beispiel des Skripts greifen wir im Kapitel über
+Körpererweiterungen wieder auf: $`x^n - p` ist irreduzibel und
+deshalb das Minimalpolynom von $`\sqrt[n]{p}`.

 # Übungsaufgabe

@@ -138,7 +138,7 @@ Genau dieses zweite Beispiel ist die Übung:

 Wenden Sie `xn_sub_r_irreduzibel` mit `r = p` an.  Zu zeigen bleibt
 $`p^2 \nmid p`: Aus $`p = p^2 \cdot c` folgt durch Kürzen
-$`1 = p \cdot c` — dann wäre $`p` eine Einheit, im Widerspruch zur
+$`1 = p \cdot 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
@@ -33,7 +33,7 @@ $`U \cdot N` für normales $`N` wieder eine Untergruppe ist.
  Mitgliedschaft schreibt sich `g ∈ U`.  Dass `U` unter Verknüpfung
  und Inversen abgeschlossen ist, sagen `U.mul_mem` und `U.inv_mem`.

-* Ein Gruppenmorphismus ist ein Term `φ : G →* Q` — ein „Bündel“ aus
+* Ein Gruppenmorphismus ist ein Term `φ : G →* Q`, ein „Bündel“ aus
  der Abbildung und den Nachweisen `map_mul : φ (a·b) = φ a · φ b`
  (daraus folgen `map_one` und `map_inv`).  Der Kern heißt `φ.ker`;
  die Mitgliedschaft entpackt
@@ -74,7 +74,7 @@ Mathlib kennt diese Aussage als Instanz
 `MonoidHom.normal_ker : φ.ker.Normal`.  Das Skript fährt fort:
 Untergruppen mit dieser Eigenschaft heißen _normale Untergruppen_
 oder _Normalteiler_, und die Bedingung ist nicht nur notwendig,
-sondern auch hinreichend — zu jedem Normalteiler existiert eine
+sondern auch hinreichend: Zu jedem Normalteiler existiert eine
 Restklassengruppe.

 # Die Restklassengruppe und ihre universelle Eigenschaft
@@ -83,8 +83,8 @@ Das Skript definiert die Restklassengruppe in Kapitel 17.3 über ihre
 universelle Eigenschaft.  Mathlib stellt beides bereit: den
 Quotienten `G ⧸ N` mit der Quotientenabbildung
 `QuotientGroup.mk' N : G →* G ⧸ N`, und die universelle Eigenschaft
-als `QuotientGroup.lift` — gegeben ein Morphismus `α : G →* H` mit
-`N ≤ α.ker` erhält man den induzierten Morphismus auf dem
+als `QuotientGroup.lift`.  Gegeben ein Morphismus `α : G →* H` mit
+`N ≤ α.ker`, erhält man den induzierten Morphismus auf dem
 Quotienten:

 ```lean
@@ -139,7 +139,7 @@ theorem mul_mem_mul {G : Type*} [Group G] (U N : Subgroup G)
 # Übungsaufgabe

 Das Skript sagt, es sei „lediglich“ die Abgeschlossenheit unter der
-Verknüpfung zu zeigen — prüfen Sie den verschwiegenen Teil selbst
+Verknüpfung zu zeigen.  Prüfen Sie den verschwiegenen Teil selbst
 nach: $`U \cdot N` ist auch abgeschlossen unter Inversen.  Tipp:
 $`(u \cdot n)^{-1} = u^{-1} \cdot (u \cdot n^{-1} \cdot u^{-1})`,
 und der zweite Faktor liegt nach `conj_mem` in $`N`.  Öffnen Sie `AlgebraInLean/Quotients.lean` und
@@ -32,9 +32,9 @@ schließt den Kreis zum Anfang des Kurses.
  `IsSquare (a : ZMod p)`.

 * Das Lean-Lernthema dieses Kapitels ist die Taktik `decide`:
-  Aussagen über konkrete endliche Objekte — „ist 7 ein Quadrat in
-  $`\mathbb{F}_{17}`?“ — sind _entscheidbar_, und Lean darf die
-  Antwort einfach ausrechnen.  Das Ergebnis ist ein vollwertiger
+  Aussagen über konkrete endliche Objekte sind _entscheidbar_, etwa
+  „ist 7 ein Quadrat in $`\mathbb{F}_{17}`?“.  Lean darf die Antwort
+  also einfach ausrechnen.  Das Ergebnis ist ein vollwertiger
  Beweis.

 # Das Reziprozitätsgesetz
@@ -46,12 +46,12 @@ Satz 24.2.1 des Skripts:
  die Gleichung
  $`\left(\tfrac{p}{q}\right) \cdot \left(\tfrac{q}{p}\right) = (-1)^{\frac{p-1}{2} \cdot \frac{q-1}{2}}`.

-In Mathlib: `legendreSym.quadratic_reciprocity` — dort mit den
-Exponenten `p / 2` geschrieben, was für ungerade $`p` dasselbe ist
-wie $`(p-1)/2`.  Dazu die beiden Ergänzungssätze: Der erste —
-$`\left(\tfrac{-1}{p}\right) = 1` genau für
-$`p \equiv 1 \pmod{4}` — ist in der
-Quadrat-Formulierung `ZMod.exists_sq_eq_neg_one_iff`:
+In Mathlib heißt der Satz `legendreSym.quadratic_reciprocity`.  Dort
+stehen die Exponenten als `p / 2`, was für ungerade $`p` dasselbe ist
+wie $`(p-1)/2`.  Dazu kommen die beiden Ergänzungssätze.  Der erste
+besagt, dass $`\left(\tfrac{-1}{p}\right) = 1` genau für
+$`p \equiv 1 \pmod{4}` gilt; in der Quadrat-Formulierung ist er
+`ZMod.exists_sq_eq_neg_one_iff`:

 ```lean
 example (p : ℕ) [Fact p.Prime] (hp : p % 4 ≠ 3) :
@@ -95,7 +95,7 @@ im Kapitel über den kleinen Satz von Fermat gerechnet haben.

 Ist 3 ein quadratischer Rest modulo 41?  Rechnen Sie erst von Hand
 nach dem Muster des Skript-Beispiels (mit Reziprozität und den
-Ergänzungssätzen) — und lassen Sie dann Lean Ihre Antwort bestätigen.
+Ergänzungssätzen).  Lassen Sie dann Lean Ihre Antwort bestätigen.
 Öffnen Sie `AlgebraInLean/Reciprocity.lean` und ersetzen Sie das
 `sorry` durch einen Beweis.

@@ -48,10 +48,10 @@ gilt unverändert weiter.
  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
+Genau dieses Argument steckt in Mathlib im Lemma
+`isIntegral_trans`: adjungiere die endlich vielen Koeffizienten
+des Minimalpolynoms, schließe auf Endlichkeit und klettere mit
+der Gradformel den Turm hinauf.  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:
@@ -89,7 +89,7 @@ Das Skript warnt an dieser Stelle:
  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
+nirgendwo ein Minimalpolynom von $`m` über $`K`.  Der Beweis von
 `isIntegral_trans` läuft über die Endlichkeit von Moduln, nicht
 über explizite Polynome.

@@ -100,8 +100,8 @@ nirgendwo ein Minimalpolynom von $`m` über $`K` — der Beweis von
   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“.
+   komponiert, und zwar mit `Module.Finite.trans`, der 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.
@@ -134,7 +134,7 @@ theorem algebraisch_quadrat {K L : Type*} [Field K]
 # 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
+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:
@@ -237,7 +237,7 @@ theorem transitivitaet_vollstaendig (K L M : Type*)

 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
+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
@@ -65,4 +65,7 @@ server as for the lecture notes.

 ## License

-CC-BY 4.0, like the lecture notes.
+CC-BY 4.0, like the lecture notes; see `LICENSE`.  The book contains an
+appendix (`Book/Appendix.lean`) restating the license and disclosing
+that these notes were produced with heavy use of AI tools, with no
+claim to originality.