feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operation polynomials for Jacobian coordinates

[Multramate]

trafficstars

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

---

• [x] depends on: #9432
• [ ] depends on: #13060

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#9432~~
• ~~leanprover-community/mathlib4#13060~~ By Dependent Issues (🤖). Happy coding!

[kbuzzard]

Thanks!

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style