Commit 2025-07-22 22:48 3e0d7050

View on Github →

chore(EllipticCurve): make affine addition computable (#27299) This allows us to compute sums, multiples, and orders of points on an elliptic curve over a field with computable operations. Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Problems.20with.20elliptic.20curves/near/529910810

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean

modified theorem WeierstrassCurve.Affine.baseChange_slope

modified theorem WeierstrassCurve.Affine.map_slope

added def WeierstrassCurve.Affine.slope

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

modified theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂

modified theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal

modified theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'

added def WeierstrassCurve.Affine.Point.add

modified theorem WeierstrassCurve.Affine.Point.toClass_injective

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean

modified theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.addX_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.addY_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean

modified theorem WeierstrassCurve.Jacobian.Point.toAffineLift_add

modified theorem WeierstrassCurve.Jacobian.Point.toAffine_add

modified theorem WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero

modified theorem WeierstrassCurve.Jacobian.add_of_X_ne

modified theorem WeierstrassCurve.Jacobian.add_of_Y_ne'

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean

modified theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.addX_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.addY_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.dblX_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.dblY_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.negAddY_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.negDblY_of_Z_ne_zero

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean

modified theorem WeierstrassCurve.Projective.Point.toAffineLift_add

modified theorem WeierstrassCurve.Projective.Point.toAffine_add

modified theorem WeierstrassCurve.Projective.addMap_of_Z_ne_zero

modified theorem WeierstrassCurve.Projective.add_of_X_ne

modified theorem WeierstrassCurve.Projective.add_of_Y_ne'