Derived from "Formalization of Geometric Algebra in HOL Light" #

This captures a fragment of this paper, and this github repo.

This file is primarily about definitions, we're not interested in the proofs used by others so much.

@[reducible]

def hol.idx (n : ℕ) :

@[protected, instance]

def hol.multivector (n : ℕ) :

Equations

Instances for hol.multivector

@[protected, instance]

def hol.multivector.module (n : ℕ) :

def hol.generic_prod {n : ℕ} (sgn : hol.idx n → hol.idx n → ℝ) (a b : hol.multivector n) :

generic product indexed by a sign function

Equations

hol.generic_prod sgn a b = finset.univ.sum (λ (ai : hol.idx n), finset.univ.sum (λ (bi : hol.idx n), pi.single (ai ∆ bi) (a ai * b bi * sgn ai bi)))

generic_prod sgn is a bilinear map

Equations

def hol.wedge {n : ℕ} :

wedge product of two multivectors

Equations

hol.wedge = hol.generic_prod (λ (ai bi : hol.idx n), ite (ai ∩ bi ≠ ∅) 0 ((-1) ^ (finset.filter (λ (abj : fin n × fin n), abj.fst > abj.snd) (ai ×ˢ bi)).card))

def hol.wedge.assoc {n : ℕ} :

wedge is associative

Note: this declaration is incomplete and uses sorry.