mathlib3

b7487a0e - feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstrass polynomials and prove basic facts (#17631)

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`). Co-authored-by: Junyan Xu <junyanxumath@gmail.com>