mathlib

d403cadd - 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.