mathlib3

6c46641d - feat(linear_algebra/clifford_algebra/fold): Add recursors for folding along generators (#14619)

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.