mul_def
plain-language theorem explainer
On the componentwise 2×2 matrices over ℤ/3ℤ used by Loom, the infix product coincides definitionally with the explicit four-entry multiplication. Anyone simplifying matrix identities for the SL(2,ℤ/3) certificate cites this. The proof is a one-line reflexivity of the instance.
Claim. For component matrices $X,Y$ with entries in $\mathbb{Z}/3\mathbb{Z}$, the notation $X * Y$ equals the explicit product $\mathrm{mul}(X,Y)$.
background
Loom is a certificate language for closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation form configurations; the computable invariant reads traces (and pairwise commutator traces) in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
Mat stores a $2\times 2$ matrix as four ZMod 3 fields rather than Mathlib's Matrix, so thousands of kernel products reduce without Finset.sum. Multiplication is therefore an explicit component formula, and the typeclass * is wired to that formula. The same mul_def pattern appears for other native number types in the foundation stack.
proof idea
One-line wrapper: rfl. The Mul instance on Mat is defined to be the bare function mul, so the equality is definitional and needs no cases or ring tactics.
why it matters
Every algebraic identity on Loom matrices opens by unfolding * via this lemma. Downstream it is the first simp step in det_mul (multiplicativity of determinant), adj_mul (adjugate reverses products, the short conjugation engine), adj_mul_of_det_one / mul_adj_of_det_one (left/right inverses when $\det=1$), and letterMat_mul_neg (generator times inverse is identity). Without a cheap unfold, the component expansions that close those proofs do not fire. In the framework this sits under the Loom invariant: trace is a class function precisely because conjugation identities reduce to ring equalities on these matrices, supporting blindness to the two non-content operations (free reduction and basepoint change) on the free group of rank 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.