mathlib

ade72abc - refactor(linear_algebra/quadratic_form/basic): generalize to semiring (#14303)

refactor(linear_algebra/quadratic_form/basic): generalize to semiring (#14303) This uses a slightly nicer strategy than the one suggested by @adamtopaz [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exterior.20algebras.20over.20semiring/near/282808284). 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.