Equational Theories
The blueprint of Equational Theories, read at commit 8b87204d (2026-11-08): one article for each of its 137 nodes whose Lean declarations it names and marks formalized, or in Mathlib. Its other 77 nodes have no article, and a section of only those is left out: the map records what the project contains, not what it plans. A statement for which the blueprint marks no proof \leanok says so. Dependencies are the blueprint's \uses: a statement's under Depends on, a proof's under Proof depends on.
The text is the blueprint's, under its Apache-2.0 license: each page has a section's prose, remarks and examples in the blueprint's order, with each node's statement and proof where the node stands.
Basic theory of magmas to Enumerating Small Finite Magmas
- Basic theory of magmas
- Selected laws
- General implications
- Implications between selected laws
- Finite implications and infinite models
- Selected magmas
- Infinite magma constructions
- Equivalence with the constant and singleton laws
- Metatheorems from Invariants
- Some abstract nonsense
- Magma cohomology
- Weak central groupoids
- Equation 854
- Equation 906
- Equation 1323
- Equation 1729
- Order 5 Austin laws
- Simple rewrites
- Trivial auto-generated theorems
- Enumerating Small Finite Magmas
Equation Search to Hard implications
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.