-- Wurzeldokument der Kursnotizen: `lake exe algebrainlean
-- --output _out` rendert sie nach `_out/html-multi`.
import VersoManual

import Book.Basics
import Book.Quotients
import Book.Ideals
import Book.Polynomials
import Book.Degrees
import Book.Elements
import Book.Transitivity
import Book.LittleFermat
import Book.Cauchy
import Book.Frobenius
import Book.Galois
import Book.Reciprocity
import Book.Appendix

open Verso.Genre Manual

#doc (Manual) "Algebra in Lean" =>
%%%
tag := "algebra-in-lean"
authors := ["Stefan Kebekus"]
%%%

Dies sind Kursnotizen zum Formalisieren von Algebra mit dem
interaktiven Theorembeweiser [Lean](https://lean-lang.org) und seiner
Mathematikbibliothek [Mathlib](https://leanprover-community.github.io).
Sie begleiten die Vorlesung _Algebra und Zahlentheorie_ (Universität
Freiburg, Winter 2026/27) mit ihrem deutschsprachigen Skript und sind
dafür gedacht, parallel zum Kurs
[_Interactive Theorem Proving using Lean_](https://pfaffelh.github.io/leancourse/)
von Peter Pfaffelhuber gelesen zu werden, der Lean selbst einführt.
Wir gehen hier den komplementären Weg: Wir nehmen an, dass Sie gerade
die _Algebra_ lernen, und zeigen an Beispielen, dass sich der Stoff der
Vorlesung mit vertretbarem Aufwand formalisieren lässt — und dass das
sogar richtig Spaß machen kann.

*Wie diese Notizen funktionieren.*  Ausgewählte Beweise aus dem Skript
werden _Satz für Satz_ nach Lean übersetzt: Jeder deutsche Originalsatz
steht als Kommentar direkt über dem Lean-Code, der ihn umsetzt.  Sie
werden sehen, dass die Standardphrasen eines Vorlesungsbeweises —
„Ansonsten liefert die Restklasse …“, „Nach dem Satz von Lagrange …“,
„Also existiert mindestens ein …“ — wiedererkennbaren Zügen in Lean
entsprechen.  Jedes Kapitel endet mit einer Übungsaufgabe, deren
`sorry` Sie durch einen Beweis ersetzen sollen.

*Woher bekomme ich das Material?*  Die Übungsdateien liegen im selben
Repository wie diese Notizen, im Ordner `AlgebraInLean/`:

```
git clone https://git.cplx.vm.uni-freiburg.de/kebekus/AlgebraInLean.git
cd AlgebraInLean
lake exe cache get
code .
```

Öffnen Sie dann zum Beispiel `AlgebraInLean/LittleFermat.lean`.
Warten Sie, bis die orangefarbenen Balken verschwinden; setzen Sie den
Cursor in einen Beweis und beobachten Sie, wie das _Infoview_-Panel
den aktuellen Beweiszustand anzeigt.  Für die Installation von Lean
und VS Code selbst folgen Sie der
[Anleitung der Lean-Community](https://leanprover-community.github.io/get_started.html)
oder der ausführlichen Anleitung am Anfang der
[Notizen von Peter Pfaffelhuber](https://pfaffelh.github.io/leancourse/).

{include 0 Book.Basics}

{include 0 Book.Quotients}

{include 0 Book.Ideals}

{include 0 Book.Polynomials}

{include 0 Book.Degrees}

{include 0 Book.Elements}

{include 0 Book.Transitivity}

{include 0 Book.LittleFermat}

{include 0 Book.Cauchy}

{include 0 Book.Frobenius}

{include 0 Book.Galois}

{include 0 Book.Reciprocity}

{include 0 Book.Appendix}