Contraction in Clifford Algebras #
Most of the results are now
upstream in linear_algebra.clifford_algebra.contraction
as of https://github.com/leanprover-community/mathlib/pull/11468.
theorem
clifford_algebra.change_form_reverse
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(d : module.dual R M)
(x : clifford_algebra Q) :
Theorem 24
Note: this declaration is incomplete and uses sorry.
def
clifford_algebra.wedge
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
[invertible 2]
(x y : clifford_algebra Q) :
The wedge product of the clifford algebra.
Equations
- x ⋏ y = ⇑((clifford_algebra.equiv_exterior Q).symm) (⇑(clifford_algebra.equiv_exterior Q) x * ⇑(clifford_algebra.equiv_exterior Q) y)