mathlib3

d46774d4 - feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors (#16153)