Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 14:14 6e016d21

View on Github →

feat(linear_algebra/{tensor,exterior,clifford}_algebra): these algebras are graded by powers of the submodules of their generators (#11542) This shows that:

  • The tensor and exterior algebras are nat-graded algebras, with each grade n corresponding to the submodule (ι R).range ^ n
  • The clifford algebra is a superalgebra (zmod 2-graded algebra), with even and odd grades corresponding to even and odd powers of the submodule (ι Q).range Eventually we'll also want to show that the tensor algebra is also graded with pieces in pi_tensor_prod, but that's a job for another time.

Estimated changes