Theorem WeierstrassCurve.Jacobian.add_of_Y_ne'

Modification history

2025-07-22 22:48

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean

chore(EllipticCurve): make affine addition computable (#27299) …

Modified WeierstrassCurve.Jacobian.add_of_Y_ne'View on Github →

2025-03-05 17:37

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

chore(AlgebraicGeometry/EllipticCurve/Jacobian/*): split Jacobian files (#22545)

Modified WeierstrassCurve.Jacobian.add_of_Y_ne'View on Github →

2024-06-06 07:00

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on point representatives for Jacobian coordinates (#9435) …

Added WeierstrassCurve.Jacobian.add_of_Y_ne'View on Github →