| ← Ch. 5: Rigor Check | Table of contents | Ch. 7: Group Theorems → |
Learning objectives. By the end of this chapter, translate the
mathematical definition of a group into a Lean structure field by
field, build both an abelian (Int) and a genuinely non-abelian
(permutations of Fin 3) example from scratch, and articulate why
bundling data with proof obligations pays off once theorems are proved
generically (Chapter 7).
Sections
- The mathematical definition
- Translating the definition into a Lean
structure - A first example: the integers under addition
- A non-abelian example: permutations of three elements
- Accessing the fields
- Why bundle proofs with data at all?
- Exercises
Starting with this chapter, most examples are followed by a “Mathlib equivalent” box (see 00-setup/04-mathlib-note.md). For links to the official docs for every Mathlib name used in those boxes, see the tactic and library reference.
| ← Ch. 5: Rigor Check | Table of contents | Ch. 7: Group Theorems → |