feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on point representatives for Jacobian coordinates

[Multramate]

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

---

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

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

[github-actions[bot]]

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

[github-actions[bot]]

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

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style