remark. [ca-0007]
remark. [ca-0007]
In literatures, \(M\) is often written \(V\), and the quotient is taken by the two-sided ideal \(I_Q\) generated from the set \(\{ v \otimes v - Q(v) \vert v \in V \}\). See also Clifford algebra [pr-spin].
As of writing, \(\textsf {Mathlib}\) does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the ring quotient by a suitable closure of a relation like \(v \otimes v \sim Q(v)\).
Hence the definition above.