Commit 2022-06-17 15:08 ade72abc

refactor(linear_algebra/quadratic_form/basic): generalize to semiring (#14303) This uses a slightly nicer strategy than the one suggested by @adamtopaz on Zulip. The main motivation here is to be able to talk about 0 : quadratic_form R M even when there is no negation available, as that will let us merge clifford_algebra (which currently requires negation) and exterior_algebra (which does not). It's likely this generalization is broadly not very useful, so this adds a quadratic_form.of_polar constructor to preserve the old more convenient API. Note the .bib file changed slightly as I ran the autoformatting tool.