Learning objectives. By the end of this chapter, translate the ring
axioms into a Lean structure built on top of CommGroup, build both a
commutative (Int, Fin 3) and a genuinely noncommutative ($2\times 2$
matrices) example from scratch, and recognize when a finite carrier lets
decide replace a hand-written proof.
Sections
- The mathematical definition
CommGroup: extending Group with one extra axiomRing: bundling an additive CommGroup with multiplication- Example: the integers as a ring
- Example: a finite commutative ring, $\mathbb{Z}/3\mathbb{Z}$
- Accessing nested fields
- Example: 2×2 matrices — a genuinely noncommutative ring
- Exercises