Commit 2022-05-19 16:29 d403cadd

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.