3.3. Exterior algebras and powers🔗

The exterior algebra is:

ExteriorAlgebra R M : Type (max u_1 u_2)#check ExteriorAlgebra R M

Given a natural number n the exterior power ∧^n M is called ExteriorAlgebra.exteriorPower and it has a special notation as follows:

variable (n : ℕ)
⋀[R]^n M : Submodule R (ExteriorAlgebra R M)#check ⋀[R]^n M

Mathlib knows that these submodules constitute a grading of the exterior algebra:

ExteriorAlgebra.gradedAlgebra R M#synth GradedAlgebra (fun i ↦ ⋀[R]^i M)