mathlib3

34e450b1 - chore(linear_algebra/quadratic_form/basic): Reorder lemmas (#14326)

chore(linear_algebra/quadratic_form/basic): Reorder lemmas (#14326) This moves the `fun_like` lemmas up to the top of the file next to the `coe_to_fun` instance, and condenses some sections containing only one lemma.