# Algebra in Lean

A hands-on introduction to formalizing algebra with the proof assistant
[Lean](https://lean-lang.org) and its mathematical library
[Mathlib](https://leanprover-community.github.io).  The course accompanies
the lecture notes *Algebra und Zahlentheorie* (Stefan Kebekus,
Universität Freiburg) and is aimed at students who are learning algebra
and have little prior experience with Lean.

Selected proofs from the lecture notes are translated into Lean
*sentence by sentence*: the German original of each sentence is quoted
as a comment directly above the Lean code implementing it, so you can
see how the standard phrases of a lecture-style proof translate into
Lean/Mathlib.

## Getting started

1. [Install Lean](https://leanprover-community.github.io/get_started.html)
   (`elan`, VS Code and the Lean 4 extension).
2. Clone this repository and fetch the precompiled Mathlib cache:

   ```bash
   git clone <repository url>
   cd AlgebraInLean
   lake exe cache get
   ```

3. Open the folder in VS Code and start with
   `AlgebraInLean/LittleFermat.lean`.

## Contents

| File | Lecture notes | Topic |
|------|---------------|-------|
| `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/Degrees.lean` | Kapitel 3 | Field extensions; the tower law |
| `AlgebraInLean/Elements.lean` | Kapitel 3 | The degree of an algebraic element |
| `AlgebraInLean/Transitivity.lean` | Kapitel 3 | Transitivity of algebraicity |
| `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 |
| `AlgebraInLean/Frobenius.lean` | Kapitel 14 | Finite fields; the Frobenius endomorphism |
| `AlgebraInLean/Galois.lean` | Kapitel 15, 16 | Galois theory; fixed fields |
| `AlgebraInLean/Reciprocity.lean` | Kapitel 24 | Quadratic reciprocity; computing Legendre symbols |

## The rendered course notes

The folder `Book/` contains the same material as a
[Verso](https://github.com/leanprover/verso) book (the technical setup
follows Peter Pfaffelhuber's
[leancourse](https://github.com/pfaffelh/leancourse)).  To render it:

```bash
lake build
lake exe algebrainlean --output _out
python3 -m http.server 8000 -d _out/html-multi   # then open http://localhost:8000
```

All Lean code in the book is elaborated during the build, so the
rendered proofs are guaranteed to compile.  `./deploy.sh` builds the
site and copies it to `public/`, which is synced to the CPLX web
server as for the lecture notes.

## License

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.