Commit 2024-10-18 18:31 df601e35

feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on point representatives for projective coordinates (#9418) 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 #8485