Commit 2025-05-07 05:50 49936c85

chore(AlgebraicGeometry/EllipticCurve/Affine/*): split affine files (#21356) The files Jacobian.lean and Projective.lean are getting too long, and are expecting even more code in the near future, so I believe this is a good time to split them. Naturally, Affine.lean and Group.lean will be refactored in a similar fashion.

• Refactor Affine.lean and Group.lean into Affine/Basic.lean (API for equations and nonsingularity), Affine/Formula.lean (formulae for group operations), and Affine/Point.lean (API for points and the group law) Note that material on the coordinate ring will very likely be refactored to another file Affine/Universal.lean in the near future, since this PR is large enough already. The other files are handled in other PRs.
• #22545 splits Jacobian.lean into Jacobian/Basic.lean (API for weighted triples, equations, and nonsingularity), Jacobian/Formula.lean (formulae for group operations), and Jacobian/Point.lean (API for points and the group law)
• #22549 splits Projective.lean into Projective/Basic.lean (API for unweighted triples, equations, and nonsingularity), Projective/Formula.lean (formulae for group operations), and Projective/Point.lean (API for points and the group law)