Commit 2022-12-19 09:05 b7487a0e

feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstrass 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).