Commit 2021-02-01 12:31 866e4fda

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.