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.

Author: eric-wieser

docs/references.bib

@@ -521,7 +521,7 @@ @Book{            Elephant
   publisher     = {Oxford University Press}
 }
 
-@book{            engel1997,
+@Book{            engel1997,
   title         = {Sperner theory},
   author        = {Engel, Konrad},
   publisher     = {Cambridge University Press},
@@ -539,22 +539,22 @@ @Article{         erdosrenyisos
   url           = {https://www.renyi.hu/~p_erdos/1966-06.pdf}
 }
 
-@article {etemadi_strong_law,
-    AUTHOR = {Etemadi, Nasrollah},
-     TITLE = {An elementary proof of the strong law of large numbers},
-   JOURNAL = {Z. Wahrsch. Verw. Gebiete},
-  FJOURNAL = {Zeitschrift f\"{u}r Wahrscheinlichkeitstheorie und Verwandte
-              Gebiete},
-    VOLUME = {55},
-      YEAR = {1981},
-    NUMBER = {1},
-     PAGES = {119--122},
-      ISSN = {0044-3719},
-   MRCLASS = {60F15 (60B12)},
-  MRNUMBER = {606010},
-MRREVIEWER = {Robert L. Taylor},
-       DOI = {10.1007/BF01013465},
-       URL = {https://doi.org/10.1007/BF01013465},
+@Article{         etemadi_strong_law,
+  author        = {Etemadi, Nasrollah},
+  title         = {An elementary proof of the strong law of large numbers},
+  journal       = {Z. Wahrsch. Verw. Gebiete},
+  fjournal      = {Zeitschrift f\"{u}r Wahrscheinlichkeitstheorie und
+                  Verwandte Gebiete},
+  volume        = {55},
+  year          = {1981},
+  number        = {1},
+  pages         = {119--122},
+  issn          = {0044-3719},
+  mrclass       = {60F15 (60B12)},
+  mrnumber      = {606010},
+  mrreviewer    = {Robert L. Taylor},
+  doi           = {10.1007/BF01013465},
+  url           = {https://doi.org/10.1007/BF01013465}
 }
 
 @Book{            Federer1996,
@@ -979,6 +979,19 @@ @Article{         huneke2002
   url           = {https://doi.org/10.1080/00029890.2002.11919853}
 }
 
+@Article{         izhakian2016,
+  title         = {Supertropical quadratic forms I},
+  journal       = {Journal of Pure and Applied Algebra},
+  volume        = {220},
+  number        = {1},
+  pages         = {61-93},
+  year          = {2016},
+  issn          = {0022-4049},
+  doi           = {10.1016/j.jpaa.2015.05.043},
+  url           = {https://www.sciencedirect.com/science/article/pii/S0022404915001589},
+  author        = {Zur Izhakian and Manfred Knebusch and Louis Rowen},
+}
+
 @Book{            james1999,
   author        = {James, Ioan},
   title         = {Topologies and uniformities},
@@ -1545,7 +1558,7 @@ @Book{            soare1987
   doi           = {10.1007/978-3-662-02460-7}
 }
 
-@book{            stanley2012,
+@Book{            stanley2012,
   author        = {Stanley, Richard P.},
   title         = {Enumerative combinatorics},
   place         = {Cambridge},