Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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>
- Loading branch information