Mathlib v3 is deprecated. Go to Mathlib v4

Theorem weierstrass_curve.point.add_def

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.add_def View on Github →