← Ch. 9: Ring Theorems

Table of contents

Ch. 11: Path Algebras →

---

Learning objectives. By the end of this chapter, translate the module axioms into a Lean structure parameterized by an explicit ring, build a Submodule as a membership predicate with closure proofs, define a LinearMap and check its two defining properties, and assemble a direct sum of modules field by field via congr 1.

Sections

1. The mathematical definition
2. Translating into Lean
3. Example: every abelian group is a $\mathbb{Z}$-module
4. Submodules
5. Linear maps
6. Direct sums of modules
7. Exercises

---

← Ch. 9: Ring Theorems

Table of contents

Ch. 11: Path Algebras →