Mathlib v3 is deprecated. Go to Mathlib v4

Theorem weierstrass_curve.point.some_add_self_of_Y_ne

Modification history

2023-02-10 16:39

src/algebraic_geometry/elliptic_curve/point.lean

feat(algebraic_geometry/elliptic_curve/point): define addition of K-rational points (#17194) …

Added weierstrass_curve.point.some_add_self_of_Y_ne View on Github →