mathlib3

d04af204 - feat(linear_algebra/quadratic_form): add lemmas about sums of quadratic forms (#7417)