refactor(AlgebraicGeometry/EllipticCurve/*): split EllipticCurve.Poin…

…t 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.

Mathlib.lean

@@ -479,7 +479,8 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.AlgebraicGeometry.AffineScheme
-import Mathlib.AlgebraicGeometry.EllipticCurve.Point
+import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
+import Mathlib.AlgebraicGeometry.EllipticCurve.Group
 import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 import Mathlib.AlgebraicGeometry.FunctionField
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction