mathlib3

a3b39c6e - feat(linear_algebra/clifford_algebra/conjugation): add lemmas showing interaction between `involute` and `even_odd` (#12672)

feat(linear_algebra/clifford_algebra/conjugation): add lemmas showing interaction between `involute` and `even_odd` (#12672) Often the even and odd submodules are defined in terms of involution, but this strategy doesn't actually work in characteristic two.