Commit 2022-07-29 05:53 56199b7b
View on Github →feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790) The main three results here are:
even.lift : even_hom Q A ≃ (clifford_algebra.even Q →ₐ[R] A)
equiv_even : clifford_algebra Q ≃ₐ[R] clifford_algebra.even (Q' Q)
even_equiv_even_neg : clifford_algebra.even Q ≃ₐ[R] clifford_algebra.even (-Q)