mathlib

56199b7b - feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790)

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)`