1 Preliminaries
This section introduces the algebraic environment of Clifford Algebra, covering vector spaces, groups, algebras, representations, modules, multilinear algebras, quadratic forms, filtrations and graded algebras.
The material in this section should be familiar to the reader, but it is worth reading through it to become familiar with the notation and terminology that is used, as well as their counterparts in Lean, which usually require some additional treatment, both mathematically and technically (probably applicable to other formal proof verification systems).
Details can be found in the references in corresponding section, or you may hover a definition/theorem, then click on L∃∀N for the Lean 4 code.
In this section, we follow [ Jadczyk(2019) ] , with supplements from [ Garling(2011) , Chen(2016) ] , and modifications to match the counterparts in Lean’s Mathlib .
We unify the informal mathematical language for a definition to:
Let \(A\) be a concept \(A\). A concept \(B\) is a set/pair/triple/tuple \((B, \mathtt{op}, ...)\), satisfying:
\(B\) is a concept \(C\) over \(A\) under op .
formula for all elements in \(B\) ( property ).
for each element in concept \(A\) there exists element such that formula for all elements in concept \(B\).
op is called op name, for all elements in \(B\), we have
formula
formula
( property ).
By default, \(A\) is a set, op is a binary operation on \(A\).