Commit 2024-11-15 06:49 50c6b5c4

feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on nonsingular rational points for projective coordinates (#9420) 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 #8485