Commit 2024-06-06 07:00 0d0c5f06

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on point representatives for Jacobian coordinates (#9435) Define the analogous secant-and-tangent negation neg and addition add on PointRep over F, and lift them to PointClass. Define Point as a PointClass that is nonsingular. Prove in neg_equiv and add_equiv that these operations preserve the equivalence. Prove in nonsingular_neg and nonsingular_add that these operations preserve nonsingularity by reducing it to the affine case, and lift these proofs to PointClass. This is the third in a series of four PRs leading to #9405 and is analogous to #9418