mathlib

866e4fda - chore(linear_algebra/quadratic_form): add two missing simp lemmas about subtraction (#5985)

chore(linear_algebra/quadratic_form): add two missing simp lemmas about subtraction (#5985) This also reorders the instance definitions to keep the lemmas about subtraction near the ones about negation, and uses the `add := (+)` pattern to make definitions unfold more nicely, even though it probably doesn't make any difference.