Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and choose a basis \(b\) indexed by a linearly ordered type. Write \(E_b(s)\) for the exterior-basis vector indexed by a finite subset \(s\). For a quadratic form \(Q\), the Mathlib linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\) gives a coordinate basis
\[B_{Q,b}(s) = \operatorname {equivExterior}(Q)^{-1}(E_b(s)).\]
This basis is transported through a linear equivalence. It does not say that the equivalence preserves multiplication or that Clifford multiplication becomes exterior multiplication. The basis-free construction is developed in [wieser2022formalizing].
The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].
Two calculations anchor the choice. The empty subset maps to the scalar unit,
\[B_{Q,b}(\varnothing ) = 1,\]
and a singleton maps to the corresponding Clifford generator,
\[B_{Q,b}(\{i\}) = \iota _Q(b(i)).\]
These are module-level identities: they determine the first two coordinate types but do not determine multiplication of arbitrary coordinates.
For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.