Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-10 16:39 67f92b6f

View on Github →

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

depends on: #17631
depends on: #17700
depends on: #17911

Estimated changes

Created src/algebraic_geometry/elliptic_curve/point.lean

added def elliptic_curve.point.mk

added theorem weierstrass_curve.Y_eq_of_X_eq

added theorem weierstrass_curve.Y_eq_of_Y_ne

added def weierstrass_curve.add_X

added def weierstrass_curve.add_Y'

added def weierstrass_curve.add_Y

added theorem weierstrass_curve.add_polynomial_eq

added theorem weierstrass_curve.add_polynomial_slope

added theorem weierstrass_curve.derivative_add_polynomial_slope

added theorem weierstrass_curve.equation_add'

added theorem weierstrass_curve.equation_add

added theorem weierstrass_curve.equation_add_iff

added theorem weierstrass_curve.equation_neg

added theorem weierstrass_curve.equation_neg_iff

added theorem weierstrass_curve.equation_neg_of

added theorem weierstrass_curve.eval_neg_polynomial

added def weierstrass_curve.neg_Y

added theorem weierstrass_curve.neg_Y_neg_Y

added theorem weierstrass_curve.nonsingular_add'

added theorem weierstrass_curve.nonsingular_add

added theorem weierstrass_curve.nonsingular_add_of_eval_derivative_ne_zero

added theorem weierstrass_curve.nonsingular_neg

added theorem weierstrass_curve.nonsingular_neg_iff

added theorem weierstrass_curve.nonsingular_neg_of

added theorem weierstrass_curve.point.add_def

added theorem weierstrass_curve.point.add_eq_zero

added theorem weierstrass_curve.point.add_left_neg

added def weierstrass_curve.point.neg

added theorem weierstrass_curve.point.neg_add_eq_zero

added theorem weierstrass_curve.point.neg_def

added theorem weierstrass_curve.point.neg_some

added theorem weierstrass_curve.point.neg_zero

added theorem weierstrass_curve.point.some_add_self_of_Y_eq

added theorem weierstrass_curve.point.some_add_self_of_Y_ne'

added theorem weierstrass_curve.point.some_add_self_of_Y_ne

added theorem weierstrass_curve.point.some_add_some_of_X_ne'

added theorem weierstrass_curve.point.some_add_some_of_X_ne

added theorem weierstrass_curve.point.some_add_some_of_Y_eq

added theorem weierstrass_curve.point.some_add_some_of_Y_ne'

added theorem weierstrass_curve.point.some_add_some_of_Y_ne

added theorem weierstrass_curve.point.zero_def

added inductive weierstrass_curve.point

added theorem weierstrass_curve.slope_of_X_ne

added theorem weierstrass_curve.slope_of_Y_ne

added theorem weierstrass_curve.slope_of_Y_ne_eq_eval

Modified src/algebraic_geometry/elliptic_curve/weierstrass.lean

modified theorem weierstrass_curve.coordinate_ring.basis_one

modified def weierstrass_curve.equation

modified theorem weierstrass_curve.eval_polynomial_X_zero

modified theorem weierstrass_curve.eval_polynomial_Y_zero

modified theorem weierstrass_curve.eval_polynomial_zero

modified def weierstrass_curve.function_field

modified theorem weierstrass_curve.nonsingular_zero