Commit 2024-02-23 18:48 800df68e

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement equations and nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring R as the type Fin 3 -> R, and its equivalence class PointClass as a quotient by the usual weighted scaling relation. Define the analogous equation and nonsingular predicates on Fin 3 -> F over a field F, and lift nonsingular to PointClass. This also has minimal API (e.g. it's missing many of the equation lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416