Commit 2022-06-16 15:46 6c46641d

View on Github →

feat(linear_algebra/clifford_algebra/fold): Add recursors for folding along generators (#14619) This adds clifford_algebra.fold{l,r} and clifford_algebra.{left,right}_induction. The former are analogous to list.foldl and list.foldr, while the latter are two stronger variants of clifford_algebra.induction. We don't bother duplicating these for the exterior_algebra, as a future PR will make exterior_algebra = clifford_algebra 0 true by rfl. This construction can be used to show:

clifford_algebra Q ≃ₗ[R] exterior_algebra R M (when invertible 2)
clifford_algebra Q ≃ₐ[R] clifford_algebra.even (Q' Q) (where Q' Q is a quadratic form over an augmented V) These will follow in future PRs.

Estimated changes

Modified src/linear_algebra/clifford_algebra/basic.lean

Created src/linear_algebra/clifford_algebra/fold.lean

added def clifford_algebra.foldl

added theorem clifford_algebra.foldl_algebra_map

added theorem clifford_algebra.foldl_mul

added theorem clifford_algebra.foldl_one

added theorem clifford_algebra.foldl_prod_map_ι

added theorem clifford_algebra.foldl_reverse

added theorem clifford_algebra.foldl_ι

added def clifford_algebra.foldr

added theorem clifford_algebra.foldr_algebra_map

added theorem clifford_algebra.foldr_mul

added theorem clifford_algebra.foldr_one

added theorem clifford_algebra.foldr_prod_map_ι

added theorem clifford_algebra.foldr_reverse

added theorem clifford_algebra.foldr_ι

added theorem clifford_algebra.left_induction

added theorem clifford_algebra.right_induction