feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on nonsingular rational points for Jacobian coordinates

[Multramate]

Define a addition-preserving bijection toAffine_addEquiv with the affine case to prove Point is an abelian group.

This is the fourth in a series of four PRs leading to #9405 and is analogous to #9420

---

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

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

[alreadydone]

Seems we need to add Jacobian.lean to style-exceptions (see here), or compress it (e.g. lemmas that fit in a single line, and blanks between such lemmas), or split it up.

[github-actions[bot]]

PR summary

Import changes

No significant changes to the import graph

---

Declarations diff

+ Point + X_eq_iff + Y_eq_iff + Y_eq_iff' + add + add_def + add_of_imp + add_point + fromAffine + fromAffine_some + fromAffine_zero + instAddPoint + instNegPoint + instZeroPoint + mk_point + neg + neg_def + neg_point + toAffine + toAffineAddEquiv + toAffineLift + toAffineLift_add + toAffineLift_eq + toAffineLift_neg + toAffineLift_of_Z_eq_zero + toAffineLift_of_Z_ne_zero + toAffineLift_some + toAffineLift_zero + toAffine_add + toAffine_neg + toAffine_of_Z_eq_zero + toAffine_of_Z_ne_zero + toAffine_of_equiv + toAffine_of_singular + toAffine_smul + toAffine_some + toAffine_zero + zero_def + zero_point

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[alreadydone]

Thanks 🎉 maintainer merge

[github-actions[bot]]

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

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style