feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstras…

…s polynomials and prove basic facts (#17631)

Define the Weierstrass polynomial and its partial derivatives, as well as properties of their evaluations (the Weierstrass equation and nonsingularity). Prove that a Weierstrass curve is nonsingular at every point if its discriminant is non-zero, and its coordinate ring is an integral domain (because the associated polynomial is irreducible). Fix minor issues (rename the variable `C` with the variable `W` to avoid a clash with `polynomial.C`, and generalise `two_torsion_polynomial_disc_ne_zero`).



Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

docs/references.bib

@@ -1875,6 +1875,14 @@ @Book{            serre1965
   url           = {https://doi.org/10.1007/978-1-4757-3910-7}
 }
 
+@Book{            silverman2009,
+  author        = {Silverman, Joseph},
+  publisher     = {Springer New York, NY},
+  series        = {Graduate Texts in Mathematics},
+  title         = {The Arithmetic of Elliptic Curves},
+  year          = {2009}
+}
+
 @Book{            simon2011,
   author        = {Simon, Barry},
   title         = {Convexity: An Analytic Viewpoint},