English
There is a module isomorphism from CliffordAlgebra Q to ExteriorAlgebra R M when 2 is invertible; it is defined via changeForm with associated_neg_proof.
Русский
Существут биективные соответствия между CliffordAlgebra(Q) и ExteriorAlgebra(R,M) при обратимости 2; отображение задаётся через changeForm с associated_neg_proof.
LaTeX
$$$\text{equivExterior} : CliffordAlgebra(Q) \simeq_{} ExteriorAlgebra(R,M) \quad[Invertible(2)],\; \text{equivExterior} = \text{changeFormEquiv}(\text{changeForm.associated_neg_proof})$$$
Lean4
/-- The module isomorphism to the exterior algebra.
Note that this holds more generally when `Q` is divisible by two, rather than only when `1` is
divisible by two; but that would be more awkward to use. -/
@[simp]
def equivExterior [Invertible (2 : R)] : CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M :=
changeFormEquiv changeForm.associated_neg_proof
