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 readers, 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 use the L∃∀N button to check the corresponding \(\textsf {Mathlib}\) document and Lean 4 source code.
In this section, we follow [jadczyk2019notes], with supplements from [garling2011clifford][chen2016infinitely],
and extensive modifications to match the counterparts in Lean's \(\textsf {Mathlib}\).