Commit 2024-06-02 08:30 ba4d71af

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Affine): add further map lemmas (#13356) ... and make definition and lemma names consistent with downstream files.

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

added theorem WeierstrassCurve.Affine.Point.add_of_X_ne'

added theorem WeierstrassCurve.Affine.Point.add_of_X_ne

added theorem WeierstrassCurve.Affine.Point.add_of_Y_eq

added theorem WeierstrassCurve.Affine.Point.add_of_Y_ne'

added theorem WeierstrassCurve.Affine.Point.add_of_Y_ne

added theorem WeierstrassCurve.Affine.Point.add_self_of_Y_eq

added theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne'

added theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne

modified theorem WeierstrassCurve.Affine.Point.map_injective

modified theorem WeierstrassCurve.Affine.Point.map_map

modified theorem WeierstrassCurve.Affine.Point.map_zero

deleted theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yeq

deleted theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne'

deleted theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne

deleted theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne'

deleted theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne

deleted theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yeq

deleted theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne'

deleted theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne

added theorem WeierstrassCurve.Affine.Y_eq_of_X_eq

added theorem WeierstrassCurve.Affine.Y_eq_of_Y_ne

deleted theorem WeierstrassCurve.Affine.Yeq_of_Xeq

deleted theorem WeierstrassCurve.Affine.Yeq_of_Yne

deleted def WeierstrassCurve.Affine.addY'

added theorem WeierstrassCurve.Affine.baseChange_addPolynomial

deleted theorem WeierstrassCurve.Affine.baseChange_addY'

modified theorem WeierstrassCurve.Affine.baseChange_equation

added theorem WeierstrassCurve.Affine.baseChange_eval_polynomial

added theorem WeierstrassCurve.Affine.baseChange_eval_polynomialX

added theorem WeierstrassCurve.Affine.baseChange_eval_polynomialY

added theorem WeierstrassCurve.Affine.baseChange_negAddY

added theorem WeierstrassCurve.Affine.baseChange_negPolynomial

modified theorem WeierstrassCurve.Affine.baseChange_nonsingular

added theorem WeierstrassCurve.Affine.baseChange_polynomial

added theorem WeierstrassCurve.Affine.baseChange_polynomialX

added theorem WeierstrassCurve.Affine.baseChange_polynomialY

deleted theorem WeierstrassCurve.Affine.equation_add'

added theorem WeierstrassCurve.Affine.equation_negAdd

added theorem WeierstrassCurve.Affine.map_addPolynomial

deleted theorem WeierstrassCurve.Affine.map_addY'

modified theorem WeierstrassCurve.Affine.map_equation

added theorem WeierstrassCurve.Affine.map_eval_polynomial

added theorem WeierstrassCurve.Affine.map_eval_polynomialX

added theorem WeierstrassCurve.Affine.map_eval_polynomialY

added theorem WeierstrassCurve.Affine.map_linePolynomial

added theorem WeierstrassCurve.Affine.map_negAddY

added theorem WeierstrassCurve.Affine.map_negPolynomial

modified theorem WeierstrassCurve.Affine.map_negY

modified theorem WeierstrassCurve.Affine.map_nonsingular

added theorem WeierstrassCurve.Affine.map_polynomial

added theorem WeierstrassCurve.Affine.map_polynomialX

added theorem WeierstrassCurve.Affine.map_polynomialY

modified theorem WeierstrassCurve.Affine.map_slope

added def WeierstrassCurve.Affine.negAddY

deleted theorem WeierstrassCurve.Affine.nonsingular_add'

deleted theorem WeierstrassCurve.Affine.nonsingular_add_of_eval_derivative_ne_zero

added theorem WeierstrassCurve.Affine.nonsingular_negAdd

added theorem WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero

added theorem WeierstrassCurve.Affine.slope_of_X_ne

deleted theorem WeierstrassCurve.Affine.slope_of_Xne

added theorem WeierstrassCurve.Affine.slope_of_Y_eq

added theorem WeierstrassCurve.Affine.slope_of_Y_ne

added theorem WeierstrassCurve.Affine.slope_of_Y_ne_eq_eval

deleted theorem WeierstrassCurve.Affine.slope_of_Yeq

deleted theorem WeierstrassCurve.Affine.slope_of_Yne

deleted theorem WeierstrassCurve.Affine.slope_of_Yne_eq_eval

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean