| ← Index | Next: Moving to Mathlib → |
Starting from #eval and def, this book built up, entirely from first
principles (no external library):
- a general
Groupstructure, with theorems proved for an arbitrary group (uniqueness of identity, uniqueness of inverses, $(ab)^{-1} = b^{-1}a^{-1}$), - a
CommGroupextendingGroup, - a
Ringstructure built on top ofCommGroup, with theorems for an arbitrary ring ($a \cdot 0 = 0$, $(-1)\cdot a = -a$), plus a genuinely noncommutative example ($2\times 2$ matrices), - a
Moduleover a ring, with submodules, linear maps, and direct sums, - a
Quiverand an indexed inductivePathtype, with path composition, as the combinatorial skeleton underlying a path algebra.
Nearly every proof in this book was written with explicit
rw/have/intro steps, each one marked with the axiom or prior theorem
that justified it, and no unexplained rfl. simp itself is
used sparingly outside Chapter 12’s own discussion of it, and only when a
genuine technical obstacle makes the explicit alternative not worth the
detour: Chapter 6’s Perm3.ext reaches for simp only [mk.injEq] because
core Lean generates no field-wise extensionality lemma for a plain
structure, and Chapter 11’s checkpoint project reaches for
simp only [Path.append, Path.length] because a match on an indexed
inductive type like Path reduces only through its equation lemmas, not
plain rfl, once an abstract path is involved. Both name only the exact
definitions being unfolded, standing in for a specific, known step rather
than an unknown pile of lemmas. Every other proof avoids simp entirely,
precisely to keep the discipline required for reading (or writing) a real
Lean library: when something goes wrong, the exact lemma responsible
should be identifiable.
| ← Index | Next: Moving to Mathlib → |