Commit 2024-09-19 18:18 f71d1808

feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operation polynomials for projective coordinates (#9417) Define auxiliary polynomials for the secant-and-tangent negation neg and addition add on Fin 3 -> F. Note that the group operations are defined from scratch instead of pulling back the group operations from the affine case, as this will be more convenient for rewriting and allows them to be defined over a ring. I don't see an easy way to define an analogous slope function as in Affine when there are now Z-coordinates in the polynomials. This is the second in a series of four PRs leading to #8485