mathlib

4d66277c - feat(linear_algebra/clifford_algebra/star): add a possibly-non-canonical star structure (#15866)