Commit 2025-01-30 22:16 088495ec

View on Github →

chore(AlgebraicGeometry/EllipticCurve/Jacobian): mirror changes in projective coordinates (#20037)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

added theorem WeierstrassCurve.Jacobian.Equation.map

modified theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero

modified theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne'

modified theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne

modified theorem WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY

added theorem WeierstrassCurve.Jacobian.addXYZ_X

added theorem WeierstrassCurve.Jacobian.addXYZ_Y

added theorem WeierstrassCurve.Jacobian.addXYZ_Z

modified theorem WeierstrassCurve.Jacobian.addZ_neg

modified theorem WeierstrassCurve.Jacobian.addZ_self

added theorem WeierstrassCurve.Jacobian.baseChange_add

added theorem WeierstrassCurve.Jacobian.baseChange_addX

added theorem WeierstrassCurve.Jacobian.baseChange_addXYZ

added theorem WeierstrassCurve.Jacobian.baseChange_addY

added theorem WeierstrassCurve.Jacobian.baseChange_dblU

added theorem WeierstrassCurve.Jacobian.baseChange_dblX

added theorem WeierstrassCurve.Jacobian.baseChange_dblXYZ

added theorem WeierstrassCurve.Jacobian.baseChange_dblY

added theorem WeierstrassCurve.Jacobian.baseChange_dblZ

added theorem WeierstrassCurve.Jacobian.baseChange_equation

added theorem WeierstrassCurve.Jacobian.baseChange_neg

added theorem WeierstrassCurve.Jacobian.baseChange_negAddY

added theorem WeierstrassCurve.Jacobian.baseChange_negDblY

added theorem WeierstrassCurve.Jacobian.baseChange_negY

added theorem WeierstrassCurve.Jacobian.baseChange_nonsingular

added theorem WeierstrassCurve.Jacobian.baseChange_polynomial

added theorem WeierstrassCurve.Jacobian.baseChange_polynomialX

added theorem WeierstrassCurve.Jacobian.baseChange_polynomialY

added theorem WeierstrassCurve.Jacobian.baseChange_polynomialZ

added theorem WeierstrassCurve.Jacobian.comp_equiv_comp

modified theorem WeierstrassCurve.Jacobian.comp_fin3

added theorem WeierstrassCurve.Jacobian.comp_smul

added theorem WeierstrassCurve.Jacobian.dblXYZ_X

added theorem WeierstrassCurve.Jacobian.dblXYZ_Y

added theorem WeierstrassCurve.Jacobian.dblXYZ_Z

modified theorem WeierstrassCurve.Jacobian.dblXYZ_smul

added theorem WeierstrassCurve.Jacobian.map_addU

modified theorem WeierstrassCurve.Jacobian.map_addX

modified theorem WeierstrassCurve.Jacobian.map_addXYZ

modified theorem WeierstrassCurve.Jacobian.map_addY

modified theorem WeierstrassCurve.Jacobian.map_addZ

modified theorem WeierstrassCurve.Jacobian.map_dblU

modified theorem WeierstrassCurve.Jacobian.map_dblX

modified theorem WeierstrassCurve.Jacobian.map_dblXYZ

modified theorem WeierstrassCurve.Jacobian.map_dblY

modified theorem WeierstrassCurve.Jacobian.map_dblZ

added theorem WeierstrassCurve.Jacobian.map_equation

modified theorem WeierstrassCurve.Jacobian.map_negAddY

modified theorem WeierstrassCurve.Jacobian.map_negDblY

modified theorem WeierstrassCurve.Jacobian.map_negY

added theorem WeierstrassCurve.Jacobian.map_nonsingular

modified theorem WeierstrassCurve.Jacobian.negAddY_eq'

modified theorem WeierstrassCurve.Jacobian.negAddY_self

modified theorem WeierstrassCurve.Jacobian.negMap_eq

added theorem WeierstrassCurve.Jacobian.negY_eq

modified theorem WeierstrassCurve.Jacobian.negY_smul

added theorem WeierstrassCurve.Jacobian.neg_X

added theorem WeierstrassCurve.Jacobian.neg_Y

added theorem WeierstrassCurve.Jacobian.neg_Z

added theorem WeierstrassCurve.Jacobian.smul_equiv_smul

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

added theorem WeierstrassCurve.Projective.baseChange_neg