Commit 2023-12-04 20:27 3399e7d9

refactor(AlgebraicGeometry/EllipticCurve/*): split EllipticCurve.Point into two files (#8540) Refactor the files in AlgebraicGeometry/EllipticCurve/* as follows:

• Weierstrass.lean contains general definitions common to all Weierstrass and elliptic curves, namely quantities associated to their coefficients, variable and base changes, and models with prescribed j-invariants.
• Affine.lean contains definitions specific to Weierstrass curves written in affine coordinates, including equation and nonsingular from the old Weierstrass.lean, but also the Point inductive and group operations from the old Point.lean.
• Group.lean contains a standalone proof of the group law for Point, including instances for CoordinateRing in the old Weierstrass.lean, and ideal computations in its ClassGroup in the old Point.lean. This refactor is done in preparation for the new Projective.lean in #8485 (and the upcoming Jacobian.lean), which shares all the general definitions in Weierstrass.lean, but none of those in Affine.lean and Group.lean except their proofs (analogous lemmas are proven by "reducing to the affine case"). Most of the definitions and lemmas for equation, nonsingular, CoordinateRing, and ClassGroup are specific to the affine representation of Weierstrass curves, so they are now in the WeierstrassCurve.Affine namespace, which is just an abbreviation for WeierstrassCurve. Further documentation is added to Group.lean to explain the argument for the group law, but otherwise few things are changed from the original files.