Commit 2024-06-10 19:34 6e0fcfb1

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group law for Jacobian coordinates (#9405) Completes the proof of the group law in Jacobian coordinates, analogously to #8485

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

deleted theorem WeierstrassCurve.Affine.Point.add_assoc

deleted theorem WeierstrassCurve.Affine.Point.add_comm

deleted theorem WeierstrassCurve.Affine.Point.add_eq_zero

deleted theorem WeierstrassCurve.Affine.Point.add_left_neg

deleted theorem WeierstrassCurve.Affine.Point.neg_add_eq_zero

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

modified theorem WeierstrassCurve.Jacobian.Point.toAffineLift_add

modified theorem WeierstrassCurve.Jacobian.Point.toAffineLift_neg

Modified scripts/style-exceptions.txt