Mathlib Phrasebook

3. Clifford, exterior algebras🔗

We describe Mathlib's theory of Clifford algebras. We also describe the exterior algebra, which is implemented as the Clifford algebra of the trivial quadratic form.

  1. 3.1. Clifford algebras
  2. 3.2. The universal property
  3. 3.3. Exterior algebras and powers