Commit 2024-06-10 11:04 0fa3e41e
View on Github →feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on nonsingular rational points for Jacobian coordinates (#9436)
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