Commit 2025-03-05 17:37 2d5df61a

View on Github →

chore(AlgebraicGeometry/EllipticCurve/Jacobian/*): split Jacobian files (#22545)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

Deleted Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

deleted theorem WeierstrassCurve.Jacobian.Equation.map

deleted def WeierstrassCurve.Jacobian.Equation

deleted def WeierstrassCurve.Jacobian.Nonsingular

deleted def WeierstrassCurve.Jacobian.NonsingularLift

deleted theorem WeierstrassCurve.Jacobian.Point.add_def

deleted theorem WeierstrassCurve.Jacobian.Point.add_point

deleted def WeierstrassCurve.Jacobian.Point.fromAffine

deleted theorem WeierstrassCurve.Jacobian.Point.fromAffine_some

deleted theorem WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero

deleted theorem WeierstrassCurve.Jacobian.Point.fromAffine_zero

deleted theorem WeierstrassCurve.Jacobian.Point.mk_ne_zero

deleted theorem WeierstrassCurve.Jacobian.Point.mk_point

deleted def WeierstrassCurve.Jacobian.Point.neg

deleted theorem WeierstrassCurve.Jacobian.Point.neg_def

deleted theorem WeierstrassCurve.Jacobian.Point.neg_point

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_add

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_eq

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_neg

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_some

deleted theorem WeierstrassCurve.Jacobian.Point.toAffineLift_zero

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_add

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_neg

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_of_equiv

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_of_singular

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_smul

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_some

deleted theorem WeierstrassCurve.Jacobian.Point.toAffine_zero

deleted theorem WeierstrassCurve.Jacobian.Point.zero_def

deleted theorem WeierstrassCurve.Jacobian.Point.zero_point

deleted structure WeierstrassCurve.Jacobian.Point

deleted theorem WeierstrassCurve.Jacobian.X_eq_iff

deleted theorem WeierstrassCurve.Jacobian.X_eq_of_equiv

deleted theorem WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.Y_eq_iff'

deleted theorem WeierstrassCurve.Jacobian.Y_eq_iff

deleted theorem WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne'

deleted theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.Y_eq_of_equiv

deleted theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne'

deleted theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY

deleted theorem WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY

deleted theorem WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv

deleted theorem WeierstrassCurve.Jacobian.addMap_eq

deleted theorem WeierstrassCurve.Jacobian.addMap_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero

deleted def WeierstrassCurve.Jacobian.addU

deleted theorem WeierstrassCurve.Jacobian.addU_ne_zero_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addU_smul

deleted def WeierstrassCurve.Jacobian.addX

deleted theorem WeierstrassCurve.Jacobian.addXYZ_X

deleted theorem WeierstrassCurve.Jacobian.addXYZ_Y

deleted theorem WeierstrassCurve.Jacobian.addXYZ_Z

deleted theorem WeierstrassCurve.Jacobian.addXYZ_neg

deleted theorem WeierstrassCurve.Jacobian.addXYZ_of_X_eq

deleted theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.addXYZ_self

deleted theorem WeierstrassCurve.Jacobian.addXYZ_smul

deleted theorem WeierstrassCurve.Jacobian.addX_eq'

deleted theorem WeierstrassCurve.Jacobian.addX_eq

deleted theorem WeierstrassCurve.Jacobian.addX_neg

deleted theorem WeierstrassCurve.Jacobian.addX_of_X_eq'

deleted theorem WeierstrassCurve.Jacobian.addX_of_X_eq

deleted theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.addX_self

deleted theorem WeierstrassCurve.Jacobian.addX_smul

deleted def WeierstrassCurve.Jacobian.addY

deleted theorem WeierstrassCurve.Jacobian.addY_neg

deleted theorem WeierstrassCurve.Jacobian.addY_of_X_eq'

deleted theorem WeierstrassCurve.Jacobian.addY_of_X_eq

deleted theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.addY_self

deleted theorem WeierstrassCurve.Jacobian.addY_smul

deleted def WeierstrassCurve.Jacobian.addZ

deleted theorem WeierstrassCurve.Jacobian.addZ_ne_zero_of_X_ne

deleted theorem WeierstrassCurve.Jacobian.addZ_neg

deleted theorem WeierstrassCurve.Jacobian.addZ_of_X_eq

deleted theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.addZ_self

deleted theorem WeierstrassCurve.Jacobian.addZ_smul

deleted theorem WeierstrassCurve.Jacobian.add_equiv

deleted theorem WeierstrassCurve.Jacobian.add_of_X_ne

deleted theorem WeierstrassCurve.Jacobian.add_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.add_of_Y_ne'

deleted theorem WeierstrassCurve.Jacobian.add_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.add_of_eq

deleted theorem WeierstrassCurve.Jacobian.add_of_equiv

deleted theorem WeierstrassCurve.Jacobian.add_of_not_equiv

deleted theorem WeierstrassCurve.Jacobian.add_self

deleted theorem WeierstrassCurve.Jacobian.add_smul_equiv

deleted theorem WeierstrassCurve.Jacobian.add_smul_of_equiv

deleted theorem WeierstrassCurve.Jacobian.add_smul_of_not_equiv

deleted theorem WeierstrassCurve.Jacobian.baseChange_add

deleted theorem WeierstrassCurve.Jacobian.baseChange_addX

deleted theorem WeierstrassCurve.Jacobian.baseChange_addXYZ

deleted theorem WeierstrassCurve.Jacobian.baseChange_addY

deleted theorem WeierstrassCurve.Jacobian.baseChange_dblU

deleted theorem WeierstrassCurve.Jacobian.baseChange_dblX

deleted theorem WeierstrassCurve.Jacobian.baseChange_dblXYZ

deleted theorem WeierstrassCurve.Jacobian.baseChange_dblY

deleted theorem WeierstrassCurve.Jacobian.baseChange_dblZ

deleted theorem WeierstrassCurve.Jacobian.baseChange_equation

deleted theorem WeierstrassCurve.Jacobian.baseChange_neg

deleted theorem WeierstrassCurve.Jacobian.baseChange_negAddY

deleted theorem WeierstrassCurve.Jacobian.baseChange_negDblY

deleted theorem WeierstrassCurve.Jacobian.baseChange_negY

deleted theorem WeierstrassCurve.Jacobian.baseChange_nonsingular

deleted theorem WeierstrassCurve.Jacobian.baseChange_polynomial

deleted theorem WeierstrassCurve.Jacobian.baseChange_polynomialX

deleted theorem WeierstrassCurve.Jacobian.baseChange_polynomialY

deleted theorem WeierstrassCurve.Jacobian.baseChange_polynomialZ

deleted theorem WeierstrassCurve.Jacobian.comp_equiv_comp

deleted theorem WeierstrassCurve.Jacobian.comp_fin3

deleted theorem WeierstrassCurve.Jacobian.comp_smul

deleted theorem WeierstrassCurve.Jacobian.dblU_eq

deleted theorem WeierstrassCurve.Jacobian.dblU_ne_zero_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.dblU_smul

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_X

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_Y

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_Z

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq'

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.dblXYZ_smul

deleted theorem WeierstrassCurve.Jacobian.dblX_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.dblX_smul

deleted theorem WeierstrassCurve.Jacobian.dblY_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.dblY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.dblY_smul

deleted def WeierstrassCurve.Jacobian.dblZ

deleted theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne'

deleted theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.dblZ_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.dblZ_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.dblZ_smul

deleted theorem WeierstrassCurve.Jacobian.equation_iff

deleted theorem WeierstrassCurve.Jacobian.equation_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.equation_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.equation_of_equiv

deleted theorem WeierstrassCurve.Jacobian.equation_smul

deleted theorem WeierstrassCurve.Jacobian.equation_some

deleted theorem WeierstrassCurve.Jacobian.equation_zero

deleted theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq'

deleted theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq

deleted theorem WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.eval_polynomial

deleted theorem WeierstrassCurve.Jacobian.eval_polynomialX

deleted theorem WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.eval_polynomialY

deleted theorem WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.eval_polynomialZ

deleted theorem WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.fin3_def

deleted theorem WeierstrassCurve.Jacobian.fin3_def_ext

deleted theorem WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne

deleted theorem WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne'

deleted theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.map_addU

deleted theorem WeierstrassCurve.Jacobian.map_addX

deleted theorem WeierstrassCurve.Jacobian.map_addXYZ

deleted theorem WeierstrassCurve.Jacobian.map_addY

deleted theorem WeierstrassCurve.Jacobian.map_addZ

deleted theorem WeierstrassCurve.Jacobian.map_dblU

deleted theorem WeierstrassCurve.Jacobian.map_dblX

deleted theorem WeierstrassCurve.Jacobian.map_dblXYZ

deleted theorem WeierstrassCurve.Jacobian.map_dblY

deleted theorem WeierstrassCurve.Jacobian.map_dblZ

deleted theorem WeierstrassCurve.Jacobian.map_equation

deleted theorem WeierstrassCurve.Jacobian.map_negAddY

deleted theorem WeierstrassCurve.Jacobian.map_negDblY

deleted theorem WeierstrassCurve.Jacobian.map_negY

deleted theorem WeierstrassCurve.Jacobian.map_nonsingular

deleted theorem WeierstrassCurve.Jacobian.map_polynomial

deleted theorem WeierstrassCurve.Jacobian.map_polynomialX

deleted theorem WeierstrassCurve.Jacobian.map_polynomialY

deleted theorem WeierstrassCurve.Jacobian.map_polynomialZ

deleted def WeierstrassCurve.Jacobian.neg

deleted def WeierstrassCurve.Jacobian.negAddY

deleted theorem WeierstrassCurve.Jacobian.negAddY_eq'

deleted theorem WeierstrassCurve.Jacobian.negAddY_eq

deleted theorem WeierstrassCurve.Jacobian.negAddY_neg

deleted theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq'

deleted theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq

deleted theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.negAddY_self

deleted theorem WeierstrassCurve.Jacobian.negAddY_smul

deleted theorem WeierstrassCurve.Jacobian.negDblY_of_Y_eq

deleted theorem WeierstrassCurve.Jacobian.negDblY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.negDblY_smul

deleted def WeierstrassCurve.Jacobian.negMap

deleted theorem WeierstrassCurve.Jacobian.negMap_eq

deleted theorem WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero

deleted def WeierstrassCurve.Jacobian.negY

deleted theorem WeierstrassCurve.Jacobian.negY_eq

deleted theorem WeierstrassCurve.Jacobian.negY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.negY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.negY_smul

deleted theorem WeierstrassCurve.Jacobian.neg_X

deleted theorem WeierstrassCurve.Jacobian.neg_Y

deleted theorem WeierstrassCurve.Jacobian.neg_Z

deleted theorem WeierstrassCurve.Jacobian.neg_equiv

deleted theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero'

deleted theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.neg_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.neg_smul_equiv

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_addMap

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_iff

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_negMap

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_some

deleted theorem WeierstrassCurve.Jacobian.nonsingularLift_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_add

deleted theorem WeierstrassCurve.Jacobian.nonsingular_iff

deleted theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Y_eq_negY

deleted theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_neg

deleted theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero

deleted theorem WeierstrassCurve.Jacobian.nonsingular_of_equiv

deleted theorem WeierstrassCurve.Jacobian.nonsingular_smul

deleted theorem WeierstrassCurve.Jacobian.nonsingular_some

deleted theorem WeierstrassCurve.Jacobian.nonsingular_zero

deleted theorem WeierstrassCurve.Jacobian.not_equiv_of_X_ne

deleted theorem WeierstrassCurve.Jacobian.not_equiv_of_Y_ne

deleted theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Jacobian.polynomialX_eq

deleted theorem WeierstrassCurve.Jacobian.polynomialY_eq

deleted theorem WeierstrassCurve.Jacobian.polynomialZ_eq

deleted theorem WeierstrassCurve.Jacobian.smul_eq

deleted theorem WeierstrassCurve.Jacobian.smul_equiv

deleted theorem WeierstrassCurve.Jacobian.smul_equiv_smul

deleted theorem WeierstrassCurve.Jacobian.smul_fin3

deleted theorem WeierstrassCurve.Jacobian.smul_fin3_ext

Created Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean

added theorem WeierstrassCurve.Jacobian.Equation.map

added def WeierstrassCurve.Jacobian.Equation

added def WeierstrassCurve.Jacobian.Nonsingular

added def WeierstrassCurve.Jacobian.NonsingularLift

added theorem WeierstrassCurve.Jacobian.X_eq_iff

added theorem WeierstrassCurve.Jacobian.X_eq_of_equiv

added theorem WeierstrassCurve.Jacobian.X_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Y_eq_iff

added theorem WeierstrassCurve.Jacobian.Y_eq_of_equiv

added theorem WeierstrassCurve.Jacobian.Y_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Z_eq_zero_of_equiv

added theorem WeierstrassCurve.Jacobian.baseChange_equation

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

added theorem WeierstrassCurve.Jacobian.comp_fin3

added theorem WeierstrassCurve.Jacobian.comp_smul

added theorem WeierstrassCurve.Jacobian.equation_iff

added theorem WeierstrassCurve.Jacobian.equation_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.equation_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.equation_of_equiv

added theorem WeierstrassCurve.Jacobian.equation_smul

added theorem WeierstrassCurve.Jacobian.equation_some

added theorem WeierstrassCurve.Jacobian.equation_zero

added theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq'

added theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq

added theorem WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq

added theorem WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.eval_polynomial

added theorem WeierstrassCurve.Jacobian.eval_polynomialX

added theorem WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.eval_polynomialY

added theorem WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.eval_polynomialZ

added theorem WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.fin3_def

added theorem WeierstrassCurve.Jacobian.fin3_def_ext

added theorem WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.map_equation

added theorem WeierstrassCurve.Jacobian.map_nonsingular

added theorem WeierstrassCurve.Jacobian.map_polynomial

added theorem WeierstrassCurve.Jacobian.map_polynomialX

added theorem WeierstrassCurve.Jacobian.map_polynomialY

added theorem WeierstrassCurve.Jacobian.map_polynomialZ

added theorem WeierstrassCurve.Jacobian.nonsingularLift_iff

added theorem WeierstrassCurve.Jacobian.nonsingularLift_some

added theorem WeierstrassCurve.Jacobian.nonsingularLift_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_iff

added theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.nonsingular_of_equiv

added theorem WeierstrassCurve.Jacobian.nonsingular_smul

added theorem WeierstrassCurve.Jacobian.nonsingular_some

added theorem WeierstrassCurve.Jacobian.nonsingular_zero

added theorem WeierstrassCurve.Jacobian.not_equiv_of_X_ne

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Y_ne

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.polynomialX_eq

added theorem WeierstrassCurve.Jacobian.polynomialY_eq

added theorem WeierstrassCurve.Jacobian.polynomialZ_eq

added theorem WeierstrassCurve.Jacobian.smul_eq

added theorem WeierstrassCurve.Jacobian.smul_equiv

added theorem WeierstrassCurve.Jacobian.smul_equiv_smul

added theorem WeierstrassCurve.Jacobian.smul_fin3

added theorem WeierstrassCurve.Jacobian.smul_fin3_ext

Created Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean

added theorem WeierstrassCurve.Jacobian.Y_eq_iff'

added theorem WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq

added theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne'

added theorem WeierstrassCurve.Jacobian.Y_eq_of_Y_ne

added theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne'

added theorem WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne

added theorem WeierstrassCurve.Jacobian.Y_sub_Y_add_Y_sub_negY

added theorem WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY

added def WeierstrassCurve.Jacobian.addU

added theorem WeierstrassCurve.Jacobian.addU_ne_zero_of_Y_ne

added theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addU_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addU_smul

added def WeierstrassCurve.Jacobian.addX

added theorem WeierstrassCurve.Jacobian.addXYZ_X

added theorem WeierstrassCurve.Jacobian.addXYZ_Y

added theorem WeierstrassCurve.Jacobian.addXYZ_Z

added theorem WeierstrassCurve.Jacobian.addXYZ_of_X_eq

added theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.addXYZ_self

added theorem WeierstrassCurve.Jacobian.addXYZ_smul

added theorem WeierstrassCurve.Jacobian.addX_eq'

added theorem WeierstrassCurve.Jacobian.addX_eq

added theorem WeierstrassCurve.Jacobian.addX_of_X_eq'

added theorem WeierstrassCurve.Jacobian.addX_of_X_eq

added theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addX_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.addX_self

added theorem WeierstrassCurve.Jacobian.addX_smul

added def WeierstrassCurve.Jacobian.addY

added theorem WeierstrassCurve.Jacobian.addY_of_X_eq'

added theorem WeierstrassCurve.Jacobian.addY_of_X_eq

added theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.addY_self

added theorem WeierstrassCurve.Jacobian.addY_smul

added def WeierstrassCurve.Jacobian.addZ

added theorem WeierstrassCurve.Jacobian.addZ_ne_zero_of_X_ne

added theorem WeierstrassCurve.Jacobian.addZ_of_X_eq

added theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addZ_self

added theorem WeierstrassCurve.Jacobian.addZ_smul

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_negAddY

added theorem WeierstrassCurve.Jacobian.baseChange_negDblY

added theorem WeierstrassCurve.Jacobian.baseChange_negY

added theorem WeierstrassCurve.Jacobian.dblU_eq

added theorem WeierstrassCurve.Jacobian.dblU_ne_zero_of_Y_eq

added theorem WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.dblU_smul

added theorem WeierstrassCurve.Jacobian.dblXYZ_X

added theorem WeierstrassCurve.Jacobian.dblXYZ_Y

added theorem WeierstrassCurve.Jacobian.dblXYZ_Z

added theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq'

added theorem WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq

added theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.dblXYZ_smul

added theorem WeierstrassCurve.Jacobian.dblX_of_Y_eq

added theorem WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.dblX_smul

added theorem WeierstrassCurve.Jacobian.dblY_of_Y_eq

added theorem WeierstrassCurve.Jacobian.dblY_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.dblY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.dblY_smul

added def WeierstrassCurve.Jacobian.dblZ

added theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne'

added theorem WeierstrassCurve.Jacobian.dblZ_ne_zero_of_Y_ne

added theorem WeierstrassCurve.Jacobian.dblZ_of_Y_eq

added theorem WeierstrassCurve.Jacobian.dblZ_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.dblZ_smul

added theorem WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne

added theorem WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne

added theorem WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq

added theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne'

added theorem WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne

added theorem WeierstrassCurve.Jacobian.map_addU

added theorem WeierstrassCurve.Jacobian.map_addX

added theorem WeierstrassCurve.Jacobian.map_addXYZ

added theorem WeierstrassCurve.Jacobian.map_addY

added theorem WeierstrassCurve.Jacobian.map_addZ

added theorem WeierstrassCurve.Jacobian.map_dblU

added theorem WeierstrassCurve.Jacobian.map_dblX

added theorem WeierstrassCurve.Jacobian.map_dblXYZ

added theorem WeierstrassCurve.Jacobian.map_dblY

added theorem WeierstrassCurve.Jacobian.map_dblZ

added theorem WeierstrassCurve.Jacobian.map_negAddY

added theorem WeierstrassCurve.Jacobian.map_negDblY

added theorem WeierstrassCurve.Jacobian.map_negY

added def WeierstrassCurve.Jacobian.negAddY

added theorem WeierstrassCurve.Jacobian.negAddY_eq'

added theorem WeierstrassCurve.Jacobian.negAddY_eq

added theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq'

added theorem WeierstrassCurve.Jacobian.negAddY_of_X_eq

added theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.negAddY_self

added theorem WeierstrassCurve.Jacobian.negAddY_smul

added theorem WeierstrassCurve.Jacobian.negDblY_of_Y_eq

added theorem WeierstrassCurve.Jacobian.negDblY_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.negDblY_smul

added def WeierstrassCurve.Jacobian.negY

added theorem WeierstrassCurve.Jacobian.negY_eq

added theorem WeierstrassCurve.Jacobian.negY_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.negY_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.negY_smul

added theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Y_eq_negY

Created Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean

added theorem WeierstrassCurve.Jacobian.Point.add_def

added theorem WeierstrassCurve.Jacobian.Point.add_point

added def WeierstrassCurve.Jacobian.Point.fromAffine

added theorem WeierstrassCurve.Jacobian.Point.fromAffine_some

added theorem WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.fromAffine_zero

added theorem WeierstrassCurve.Jacobian.Point.mk_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.mk_point

added def WeierstrassCurve.Jacobian.Point.neg

added theorem WeierstrassCurve.Jacobian.Point.neg_def

added theorem WeierstrassCurve.Jacobian.Point.neg_point

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_add

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_eq

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_neg

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_some

added theorem WeierstrassCurve.Jacobian.Point.toAffineLift_zero

added theorem WeierstrassCurve.Jacobian.Point.toAffine_add

added theorem WeierstrassCurve.Jacobian.Point.toAffine_neg

added theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.toAffine_of_equiv

added theorem WeierstrassCurve.Jacobian.Point.toAffine_of_singular

added theorem WeierstrassCurve.Jacobian.Point.toAffine_smul

added theorem WeierstrassCurve.Jacobian.Point.toAffine_some

added theorem WeierstrassCurve.Jacobian.Point.toAffine_zero

added theorem WeierstrassCurve.Jacobian.Point.zero_def

added theorem WeierstrassCurve.Jacobian.Point.zero_point

added structure WeierstrassCurve.Jacobian.Point

added theorem WeierstrassCurve.Jacobian.addMap_eq

added theorem WeierstrassCurve.Jacobian.addMap_of_Y_eq

added theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.addXYZ_neg

added theorem WeierstrassCurve.Jacobian.addX_neg

added theorem WeierstrassCurve.Jacobian.addY_neg

added theorem WeierstrassCurve.Jacobian.addZ_neg

added theorem WeierstrassCurve.Jacobian.add_equiv

added theorem WeierstrassCurve.Jacobian.add_of_X_ne

added theorem WeierstrassCurve.Jacobian.add_of_Y_eq

added theorem WeierstrassCurve.Jacobian.add_of_Y_ne'

added theorem WeierstrassCurve.Jacobian.add_of_Y_ne

added theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_left

added theorem WeierstrassCurve.Jacobian.add_of_Z_eq_zero_right

added theorem WeierstrassCurve.Jacobian.add_of_eq

added theorem WeierstrassCurve.Jacobian.add_of_equiv

added theorem WeierstrassCurve.Jacobian.add_of_not_equiv

added theorem WeierstrassCurve.Jacobian.add_self

added theorem WeierstrassCurve.Jacobian.add_smul_equiv

added theorem WeierstrassCurve.Jacobian.add_smul_of_equiv

added theorem WeierstrassCurve.Jacobian.add_smul_of_not_equiv

added theorem WeierstrassCurve.Jacobian.baseChange_add

added theorem WeierstrassCurve.Jacobian.baseChange_neg

added def WeierstrassCurve.Jacobian.neg

added theorem WeierstrassCurve.Jacobian.negAddY_neg

added def WeierstrassCurve.Jacobian.negMap

added theorem WeierstrassCurve.Jacobian.negMap_eq

added theorem WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.neg_X

added theorem WeierstrassCurve.Jacobian.neg_Y

added theorem WeierstrassCurve.Jacobian.neg_Z

added theorem WeierstrassCurve.Jacobian.neg_equiv

added theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero'

added theorem WeierstrassCurve.Jacobian.neg_of_Z_eq_zero

added theorem WeierstrassCurve.Jacobian.neg_of_Z_ne_zero

added theorem WeierstrassCurve.Jacobian.neg_smul_equiv

added theorem WeierstrassCurve.Jacobian.nonsingularLift_addMap

added theorem WeierstrassCurve.Jacobian.nonsingularLift_negMap

added theorem WeierstrassCurve.Jacobian.nonsingular_add

added theorem WeierstrassCurve.Jacobian.nonsingular_neg

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean