chore(linear_algebra/quadratic_form/basic): remove redundant fields (#14246)
chore(linear_algebra/quadratic_form/basic): remove redundant fields (#14246)

This renames `quadratic_form.mk_left` to `quadratic_form.mk` by removing the redundant fields in the structure, as the proof of `mk_left` didn't actually use the fact the ring was commutative as it claimed to in the docstring.
The only reason we could possibly want these is if addition were non-commutative, which seems extremely unlikely.





leanprover-community/mathlib,leanprover-community/mathlib