Commit 2023-07-03 05:44 c7c8ac38

View on Github →

feat: port AlgebraicGeometry.EllipticCurve.Point (#5541)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/EllipticCurve/Point.lean

added def EllipticCurve.Point.mk

added theorem WeierstrassCurve.C_addPolynomial

added theorem WeierstrassCurve.CoordinateRing.C_addPolynomial

added theorem WeierstrassCurve.CoordinateRing.C_addPolynomial_slope

added theorem WeierstrassCurve.Point.add_assoc

added theorem WeierstrassCurve.Point.add_comm

added theorem WeierstrassCurve.Point.add_def

added theorem WeierstrassCurve.Point.add_eq_zero

added theorem WeierstrassCurve.Point.add_left_neg

added def WeierstrassCurve.Point.neg

added theorem WeierstrassCurve.Point.neg_add_eq_zero

added theorem WeierstrassCurve.Point.neg_def

added theorem WeierstrassCurve.Point.neg_some

added theorem WeierstrassCurve.Point.neg_zero

added def WeierstrassCurve.Point.ofBaseChange

added def WeierstrassCurve.Point.ofBaseChangeFun

added theorem WeierstrassCurve.Point.ofBaseChange_injective

added theorem WeierstrassCurve.Point.some_add_self_of_Y_eq

added theorem WeierstrassCurve.Point.some_add_self_of_Y_ne'

added theorem WeierstrassCurve.Point.some_add_self_of_Y_ne

added theorem WeierstrassCurve.Point.some_add_some_of_X_ne'

added theorem WeierstrassCurve.Point.some_add_some_of_X_ne

added theorem WeierstrassCurve.Point.some_add_some_of_Y_eq

added theorem WeierstrassCurve.Point.some_add_some_of_Y_ne'

added theorem WeierstrassCurve.Point.some_add_some_of_Y_ne

added theorem WeierstrassCurve.Point.toClass_eq_zero

added theorem WeierstrassCurve.Point.toClass_injective

added theorem WeierstrassCurve.Point.toClass_some

added theorem WeierstrassCurve.Point.toClass_zero

added theorem WeierstrassCurve.Point.zero_def

added inductive WeierstrassCurve.Point

added theorem WeierstrassCurve.XYIdeal'_eq

added theorem WeierstrassCurve.XYIdeal_add_eq

added theorem WeierstrassCurve.XYIdeal_eq₁

added theorem WeierstrassCurve.XYIdeal_eq₂

added theorem WeierstrassCurve.XYIdeal_mul_XYIdeal

added theorem WeierstrassCurve.XYIdeal_neg_mul

added theorem WeierstrassCurve.Y_eq_of_X_eq

added theorem WeierstrassCurve.Y_eq_of_Y_ne

added theorem WeierstrassCurve.addPolynomial_eq

added theorem WeierstrassCurve.addPolynomial_slope

added def WeierstrassCurve.addX

added def WeierstrassCurve.addY'

added def WeierstrassCurve.addY

added theorem WeierstrassCurve.baseChange_addX

added theorem WeierstrassCurve.baseChange_addX_of_baseChange

added theorem WeierstrassCurve.baseChange_addY'

added theorem WeierstrassCurve.baseChange_addY'_of_baseChange

added theorem WeierstrassCurve.baseChange_addY

added theorem WeierstrassCurve.baseChange_addY_of_baseChange

added theorem WeierstrassCurve.baseChange_negY

added theorem WeierstrassCurve.baseChange_negY_of_baseChange

added theorem WeierstrassCurve.baseChange_slope

added theorem WeierstrassCurve.baseChange_slope_of_baseChange

added theorem WeierstrassCurve.derivative_addPolynomial_slope

added theorem WeierstrassCurve.equation_add'

added theorem WeierstrassCurve.equation_add

added theorem WeierstrassCurve.equation_add_iff

added theorem WeierstrassCurve.equation_neg

added theorem WeierstrassCurve.equation_neg_iff

added theorem WeierstrassCurve.equation_neg_of

added theorem WeierstrassCurve.eval_negPolynomial

added theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal'

added theorem WeierstrassCurve.mk_XYIdeal'_mul_mk_XYIdeal'_of_Y_eq

added def WeierstrassCurve.negY

added theorem WeierstrassCurve.negY_negY

added theorem WeierstrassCurve.nonsingular_add'

added theorem WeierstrassCurve.nonsingular_add

added theorem WeierstrassCurve.nonsingular_add_of_eval_derivative_ne_zero

added theorem WeierstrassCurve.nonsingular_neg

added theorem WeierstrassCurve.nonsingular_neg_iff

added theorem WeierstrassCurve.nonsingular_neg_of

added theorem WeierstrassCurve.slope_of_X_ne

added theorem WeierstrassCurve.slope_of_Y_eq

added theorem WeierstrassCurve.slope_of_Y_ne

added theorem WeierstrassCurve.slope_of_Y_ne_eq_eval

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean