Commit 2024-05-30 14:17 b1a351c3

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operation polynomials for Jacobian coordinates (#9433) 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 #9405 and is analogous to #9417