mathlib

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

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.