Commit 2025-03-04 21:14 66201572

View on Github →

chore(AlgebraicGeometry/EllipticCurve/Projective/*): split projective files (#22549)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

Deleted Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

deleted theorem WeierstrassCurve.Projective.Equation.map

deleted def WeierstrassCurve.Projective.Equation

deleted def WeierstrassCurve.Projective.Nonsingular

deleted def WeierstrassCurve.Projective.NonsingularLift

deleted theorem WeierstrassCurve.Projective.Point.add_def

deleted theorem WeierstrassCurve.Projective.Point.add_point

deleted def WeierstrassCurve.Projective.Point.fromAffine

deleted theorem WeierstrassCurve.Projective.Point.fromAffine_some

deleted theorem WeierstrassCurve.Projective.Point.fromAffine_some_ne_zero

deleted theorem WeierstrassCurve.Projective.Point.fromAffine_zero

deleted theorem WeierstrassCurve.Projective.Point.mk_ne_zero

deleted theorem WeierstrassCurve.Projective.Point.mk_point

deleted def WeierstrassCurve.Projective.Point.neg

deleted theorem WeierstrassCurve.Projective.Point.neg_def

deleted theorem WeierstrassCurve.Projective.Point.neg_point

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_add

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_eq

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_neg

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_some

deleted theorem WeierstrassCurve.Projective.Point.toAffineLift_zero

deleted theorem WeierstrassCurve.Projective.Point.toAffine_add

deleted theorem WeierstrassCurve.Projective.Point.toAffine_neg

deleted theorem WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.Point.toAffine_of_equiv

deleted theorem WeierstrassCurve.Projective.Point.toAffine_of_singular

deleted theorem WeierstrassCurve.Projective.Point.toAffine_smul

deleted theorem WeierstrassCurve.Projective.Point.toAffine_some

deleted theorem WeierstrassCurve.Projective.Point.toAffine_zero

deleted theorem WeierstrassCurve.Projective.Point.zero_def

deleted theorem WeierstrassCurve.Projective.Point.zero_point

deleted structure WeierstrassCurve.Projective.Point

deleted theorem WeierstrassCurve.Projective.X_eq_iff

deleted theorem WeierstrassCurve.Projective.X_eq_of_equiv

deleted theorem WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.Y_eq_iff'

deleted theorem WeierstrassCurve.Projective.Y_eq_iff

deleted theorem WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq

deleted theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne'

deleted theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne

deleted theorem WeierstrassCurve.Projective.Y_eq_of_equiv

deleted theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne'

deleted theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne

deleted theorem WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY

deleted theorem WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY

deleted theorem WeierstrassCurve.Projective.Z_eq_zero_of_equiv

deleted theorem WeierstrassCurve.Projective.addMap_eq

deleted theorem WeierstrassCurve.Projective.addMap_of_Y_eq

deleted theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addMap_of_Z_ne_zero

deleted def WeierstrassCurve.Projective.addU

deleted theorem WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne

deleted theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addU_smul

deleted def WeierstrassCurve.Projective.addX

deleted theorem WeierstrassCurve.Projective.addXYZ_X

deleted theorem WeierstrassCurve.Projective.addXYZ_Y

deleted theorem WeierstrassCurve.Projective.addXYZ_Z

deleted theorem WeierstrassCurve.Projective.addXYZ_neg

deleted theorem WeierstrassCurve.Projective.addXYZ_of_X_eq

deleted theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.addXYZ_self

deleted theorem WeierstrassCurve.Projective.addXYZ_smul

deleted theorem WeierstrassCurve.Projective.addX_eq'

deleted theorem WeierstrassCurve.Projective.addX_eq

deleted theorem WeierstrassCurve.Projective.addX_neg

deleted theorem WeierstrassCurve.Projective.addX_of_X_eq

deleted theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.addX_self

deleted theorem WeierstrassCurve.Projective.addX_smul

deleted def WeierstrassCurve.Projective.addY

deleted theorem WeierstrassCurve.Projective.addY_neg

deleted theorem WeierstrassCurve.Projective.addY_of_X_eq'

deleted theorem WeierstrassCurve.Projective.addY_of_X_eq

deleted theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.addY_self

deleted theorem WeierstrassCurve.Projective.addY_smul

deleted def WeierstrassCurve.Projective.addZ

deleted theorem WeierstrassCurve.Projective.addZ_eq'

deleted theorem WeierstrassCurve.Projective.addZ_eq

deleted theorem WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne

deleted theorem WeierstrassCurve.Projective.addZ_neg

deleted theorem WeierstrassCurve.Projective.addZ_of_X_eq

deleted theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.addZ_self

deleted theorem WeierstrassCurve.Projective.addZ_smul

deleted theorem WeierstrassCurve.Projective.add_equiv

deleted theorem WeierstrassCurve.Projective.add_of_X_ne

deleted theorem WeierstrassCurve.Projective.add_of_Y_eq

deleted theorem WeierstrassCurve.Projective.add_of_Y_ne'

deleted theorem WeierstrassCurve.Projective.add_of_Y_ne

deleted theorem WeierstrassCurve.Projective.add_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.add_of_eq

deleted theorem WeierstrassCurve.Projective.add_of_equiv

deleted theorem WeierstrassCurve.Projective.add_of_not_equiv

deleted theorem WeierstrassCurve.Projective.add_self

deleted theorem WeierstrassCurve.Projective.add_smul_equiv

deleted theorem WeierstrassCurve.Projective.add_smul_of_equiv

deleted theorem WeierstrassCurve.Projective.add_smul_of_not_equiv

deleted theorem WeierstrassCurve.Projective.baseChange_add

deleted theorem WeierstrassCurve.Projective.baseChange_addX

deleted theorem WeierstrassCurve.Projective.baseChange_addXYZ

deleted theorem WeierstrassCurve.Projective.baseChange_addY

deleted theorem WeierstrassCurve.Projective.baseChange_dblU

deleted theorem WeierstrassCurve.Projective.baseChange_dblX

deleted theorem WeierstrassCurve.Projective.baseChange_dblXYZ

deleted theorem WeierstrassCurve.Projective.baseChange_dblY

deleted theorem WeierstrassCurve.Projective.baseChange_dblZ

deleted theorem WeierstrassCurve.Projective.baseChange_equation

deleted theorem WeierstrassCurve.Projective.baseChange_neg

deleted theorem WeierstrassCurve.Projective.baseChange_negAddY

deleted theorem WeierstrassCurve.Projective.baseChange_negDblY

deleted theorem WeierstrassCurve.Projective.baseChange_negY

deleted theorem WeierstrassCurve.Projective.baseChange_nonsingular

deleted theorem WeierstrassCurve.Projective.baseChange_polynomial

deleted theorem WeierstrassCurve.Projective.baseChange_polynomialX

deleted theorem WeierstrassCurve.Projective.baseChange_polynomialY

deleted theorem WeierstrassCurve.Projective.baseChange_polynomialZ

deleted theorem WeierstrassCurve.Projective.comp_equiv_comp

deleted theorem WeierstrassCurve.Projective.comp_fin3

deleted theorem WeierstrassCurve.Projective.comp_smul

deleted theorem WeierstrassCurve.Projective.dblU_eq

deleted theorem WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eq

deleted theorem WeierstrassCurve.Projective.dblU_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.dblU_smul

deleted theorem WeierstrassCurve.Projective.dblXYZ_X

deleted theorem WeierstrassCurve.Projective.dblXYZ_Y

deleted theorem WeierstrassCurve.Projective.dblXYZ_Z

deleted theorem WeierstrassCurve.Projective.dblXYZ_of_Y_eq

deleted theorem WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.dblXYZ_smul

deleted theorem WeierstrassCurve.Projective.dblX_eq'

deleted theorem WeierstrassCurve.Projective.dblX_eq

deleted theorem WeierstrassCurve.Projective.dblX_of_Y_eq

deleted theorem WeierstrassCurve.Projective.dblX_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.dblX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.dblX_smul

deleted theorem WeierstrassCurve.Projective.dblY_of_Y_eq'

deleted theorem WeierstrassCurve.Projective.dblY_of_Y_eq

deleted theorem WeierstrassCurve.Projective.dblY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.dblY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.dblY_smul

deleted def WeierstrassCurve.Projective.dblZ

deleted theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne'

deleted theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne

deleted theorem WeierstrassCurve.Projective.dblZ_of_Y_eq

deleted theorem WeierstrassCurve.Projective.dblZ_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.dblZ_smul

deleted theorem WeierstrassCurve.Projective.equation_iff

deleted theorem WeierstrassCurve.Projective.equation_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.equation_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.equation_of_equiv

deleted theorem WeierstrassCurve.Projective.equation_smul

deleted theorem WeierstrassCurve.Projective.equation_some

deleted theorem WeierstrassCurve.Projective.equation_zero

deleted theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq'

deleted theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq

deleted theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq

deleted theorem WeierstrassCurve.Projective.equiv_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.eval_polynomial

deleted theorem WeierstrassCurve.Projective.eval_polynomialX

deleted theorem WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.eval_polynomialY

deleted theorem WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.eval_polynomialZ

deleted theorem WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.fin3_def

deleted theorem WeierstrassCurve.Projective.fin3_def_ext

deleted theorem WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.isUnit_addU_of_Y_ne

deleted theorem WeierstrassCurve.Projective.isUnit_addZ_of_X_ne

deleted theorem WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq

deleted theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne'

deleted theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne

deleted theorem WeierstrassCurve.Projective.map_addU

deleted theorem WeierstrassCurve.Projective.map_addX

deleted theorem WeierstrassCurve.Projective.map_addXYZ

deleted theorem WeierstrassCurve.Projective.map_addY

deleted theorem WeierstrassCurve.Projective.map_addZ

deleted theorem WeierstrassCurve.Projective.map_dblU

deleted theorem WeierstrassCurve.Projective.map_dblX

deleted theorem WeierstrassCurve.Projective.map_dblXYZ

deleted theorem WeierstrassCurve.Projective.map_dblY

deleted theorem WeierstrassCurve.Projective.map_dblZ

deleted theorem WeierstrassCurve.Projective.map_equation

deleted theorem WeierstrassCurve.Projective.map_negAddY

deleted theorem WeierstrassCurve.Projective.map_negDblY

deleted theorem WeierstrassCurve.Projective.map_negY

deleted theorem WeierstrassCurve.Projective.map_nonsingular

deleted theorem WeierstrassCurve.Projective.map_polynomial

deleted theorem WeierstrassCurve.Projective.map_polynomialX

deleted theorem WeierstrassCurve.Projective.map_polynomialY

deleted theorem WeierstrassCurve.Projective.map_polynomialZ

deleted def WeierstrassCurve.Projective.neg

deleted def WeierstrassCurve.Projective.negAddY

deleted theorem WeierstrassCurve.Projective.negAddY_eq'

deleted theorem WeierstrassCurve.Projective.negAddY_eq

deleted theorem WeierstrassCurve.Projective.negAddY_neg

deleted theorem WeierstrassCurve.Projective.negAddY_of_X_eq'

deleted theorem WeierstrassCurve.Projective.negAddY_of_X_eq

deleted theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.negAddY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.negAddY_self

deleted theorem WeierstrassCurve.Projective.negAddY_smul

deleted theorem WeierstrassCurve.Projective.negDblY_eq'

deleted theorem WeierstrassCurve.Projective.negDblY_eq

deleted theorem WeierstrassCurve.Projective.negDblY_of_Y_eq'

deleted theorem WeierstrassCurve.Projective.negDblY_of_Y_eq

deleted theorem WeierstrassCurve.Projective.negDblY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.negDblY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.negDblY_smul

deleted def WeierstrassCurve.Projective.negMap

deleted theorem WeierstrassCurve.Projective.negMap_eq

deleted theorem WeierstrassCurve.Projective.negMap_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.negMap_of_Z_ne_zero

deleted def WeierstrassCurve.Projective.negY

deleted theorem WeierstrassCurve.Projective.negY_eq

deleted theorem WeierstrassCurve.Projective.negY_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.negY_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.negY_smul

deleted theorem WeierstrassCurve.Projective.neg_X

deleted theorem WeierstrassCurve.Projective.neg_Y

deleted theorem WeierstrassCurve.Projective.neg_Z

deleted theorem WeierstrassCurve.Projective.neg_equiv

deleted theorem WeierstrassCurve.Projective.neg_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.neg_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.neg_smul_equiv

deleted theorem WeierstrassCurve.Projective.nonsingularLift_addMap

deleted theorem WeierstrassCurve.Projective.nonsingularLift_iff

deleted theorem WeierstrassCurve.Projective.nonsingularLift_negMap

deleted theorem WeierstrassCurve.Projective.nonsingularLift_some

deleted theorem WeierstrassCurve.Projective.nonsingularLift_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_add

deleted theorem WeierstrassCurve.Projective.nonsingular_iff

deleted theorem WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY

deleted theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_neg

deleted theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero

deleted theorem WeierstrassCurve.Projective.nonsingular_of_equiv

deleted theorem WeierstrassCurve.Projective.nonsingular_smul

deleted theorem WeierstrassCurve.Projective.nonsingular_some

deleted theorem WeierstrassCurve.Projective.nonsingular_zero

deleted theorem WeierstrassCurve.Projective.not_equiv_of_X_ne

deleted theorem WeierstrassCurve.Projective.not_equiv_of_Y_ne

deleted theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left

deleted theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right

deleted theorem WeierstrassCurve.Projective.polynomialX_eq

deleted theorem WeierstrassCurve.Projective.polynomialY_eq

deleted theorem WeierstrassCurve.Projective.polynomialZ_eq

deleted theorem WeierstrassCurve.Projective.polynomial_relation

deleted theorem WeierstrassCurve.Projective.smul_eq

deleted theorem WeierstrassCurve.Projective.smul_equiv

deleted theorem WeierstrassCurve.Projective.smul_equiv_smul

deleted theorem WeierstrassCurve.Projective.smul_fin3

deleted theorem WeierstrassCurve.Projective.smul_fin3_ext

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

added theorem WeierstrassCurve.Projective.Equation.map

added def WeierstrassCurve.Projective.Equation

added def WeierstrassCurve.Projective.Nonsingular

added def WeierstrassCurve.Projective.NonsingularLift

added theorem WeierstrassCurve.Projective.X_eq_iff

added theorem WeierstrassCurve.Projective.X_eq_of_equiv

added theorem WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Y_eq_iff

added theorem WeierstrassCurve.Projective.Y_eq_of_equiv

added theorem WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Z_eq_zero_of_equiv

added theorem WeierstrassCurve.Projective.baseChange_equation

added theorem WeierstrassCurve.Projective.baseChange_nonsingular

added theorem WeierstrassCurve.Projective.baseChange_polynomial

added theorem WeierstrassCurve.Projective.baseChange_polynomialX

added theorem WeierstrassCurve.Projective.baseChange_polynomialY

added theorem WeierstrassCurve.Projective.baseChange_polynomialZ

added theorem WeierstrassCurve.Projective.comp_equiv_comp

added theorem WeierstrassCurve.Projective.comp_fin3

added theorem WeierstrassCurve.Projective.comp_smul

added theorem WeierstrassCurve.Projective.equation_iff

added theorem WeierstrassCurve.Projective.equation_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.equation_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.equation_of_equiv

added theorem WeierstrassCurve.Projective.equation_smul

added theorem WeierstrassCurve.Projective.equation_some

added theorem WeierstrassCurve.Projective.equation_zero

added theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq'

added theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq

added theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq

added theorem WeierstrassCurve.Projective.equiv_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.eval_polynomial

added theorem WeierstrassCurve.Projective.eval_polynomialX

added theorem WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.eval_polynomialY

added theorem WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.eval_polynomialZ

added theorem WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.fin3_def

added theorem WeierstrassCurve.Projective.fin3_def_ext

added theorem WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.map_equation

added theorem WeierstrassCurve.Projective.map_nonsingular

added theorem WeierstrassCurve.Projective.map_polynomial

added theorem WeierstrassCurve.Projective.map_polynomialX

added theorem WeierstrassCurve.Projective.map_polynomialY

added theorem WeierstrassCurve.Projective.map_polynomialZ

added theorem WeierstrassCurve.Projective.nonsingularLift_iff

added theorem WeierstrassCurve.Projective.nonsingularLift_some

added theorem WeierstrassCurve.Projective.nonsingularLift_zero

added theorem WeierstrassCurve.Projective.nonsingular_iff

added theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.nonsingular_of_equiv

added theorem WeierstrassCurve.Projective.nonsingular_smul

added theorem WeierstrassCurve.Projective.nonsingular_some

added theorem WeierstrassCurve.Projective.nonsingular_zero

added theorem WeierstrassCurve.Projective.not_equiv_of_X_ne

added theorem WeierstrassCurve.Projective.not_equiv_of_Y_ne

added theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.polynomialX_eq

added theorem WeierstrassCurve.Projective.polynomialY_eq

added theorem WeierstrassCurve.Projective.polynomialZ_eq

added theorem WeierstrassCurve.Projective.polynomial_relation

added theorem WeierstrassCurve.Projective.smul_eq

added theorem WeierstrassCurve.Projective.smul_equiv

added theorem WeierstrassCurve.Projective.smul_equiv_smul

added theorem WeierstrassCurve.Projective.smul_fin3

added theorem WeierstrassCurve.Projective.smul_fin3_ext

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

added theorem WeierstrassCurve.Projective.Y_eq_iff'

added theorem WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq

added theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne'

added theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne

added theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne'

added theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne

added theorem WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY

added theorem WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY

added def WeierstrassCurve.Projective.addU

added theorem WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne

added theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addU_smul

added def WeierstrassCurve.Projective.addX

added theorem WeierstrassCurve.Projective.addXYZ_X

added theorem WeierstrassCurve.Projective.addXYZ_Y

added theorem WeierstrassCurve.Projective.addXYZ_Z

added theorem WeierstrassCurve.Projective.addXYZ_of_X_eq

added theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.addXYZ_self

added theorem WeierstrassCurve.Projective.addXYZ_smul

added theorem WeierstrassCurve.Projective.addX_eq'

added theorem WeierstrassCurve.Projective.addX_eq

added theorem WeierstrassCurve.Projective.addX_of_X_eq

added theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addX_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.addX_self

added theorem WeierstrassCurve.Projective.addX_smul

added def WeierstrassCurve.Projective.addY

added theorem WeierstrassCurve.Projective.addY_of_X_eq'

added theorem WeierstrassCurve.Projective.addY_of_X_eq

added theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.addY_self

added theorem WeierstrassCurve.Projective.addY_smul

added def WeierstrassCurve.Projective.addZ

added theorem WeierstrassCurve.Projective.addZ_eq'

added theorem WeierstrassCurve.Projective.addZ_eq

added theorem WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne

added theorem WeierstrassCurve.Projective.addZ_of_X_eq

added theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addZ_self

added theorem WeierstrassCurve.Projective.addZ_smul

added theorem WeierstrassCurve.Projective.baseChange_addX

added theorem WeierstrassCurve.Projective.baseChange_addXYZ

added theorem WeierstrassCurve.Projective.baseChange_addY

added theorem WeierstrassCurve.Projective.baseChange_dblU

added theorem WeierstrassCurve.Projective.baseChange_dblX

added theorem WeierstrassCurve.Projective.baseChange_dblXYZ

added theorem WeierstrassCurve.Projective.baseChange_dblY

added theorem WeierstrassCurve.Projective.baseChange_dblZ

added theorem WeierstrassCurve.Projective.baseChange_negAddY

added theorem WeierstrassCurve.Projective.baseChange_negDblY

added theorem WeierstrassCurve.Projective.baseChange_negY

added theorem WeierstrassCurve.Projective.dblU_eq

added theorem WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eq

added theorem WeierstrassCurve.Projective.dblU_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.dblU_smul

added theorem WeierstrassCurve.Projective.dblXYZ_X

added theorem WeierstrassCurve.Projective.dblXYZ_Y

added theorem WeierstrassCurve.Projective.dblXYZ_Z

added theorem WeierstrassCurve.Projective.dblXYZ_of_Y_eq

added theorem WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.dblXYZ_smul

added theorem WeierstrassCurve.Projective.dblX_eq'

added theorem WeierstrassCurve.Projective.dblX_eq

added theorem WeierstrassCurve.Projective.dblX_of_Y_eq

added theorem WeierstrassCurve.Projective.dblX_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.dblX_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.dblX_smul

added theorem WeierstrassCurve.Projective.dblY_of_Y_eq'

added theorem WeierstrassCurve.Projective.dblY_of_Y_eq

added theorem WeierstrassCurve.Projective.dblY_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.dblY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.dblY_smul

added def WeierstrassCurve.Projective.dblZ

added theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne'

added theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne

added theorem WeierstrassCurve.Projective.dblZ_of_Y_eq

added theorem WeierstrassCurve.Projective.dblZ_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.dblZ_smul

added theorem WeierstrassCurve.Projective.isUnit_addU_of_Y_ne

added theorem WeierstrassCurve.Projective.isUnit_addZ_of_X_ne

added theorem WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq

added theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne'

added theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne

added theorem WeierstrassCurve.Projective.map_addU

added theorem WeierstrassCurve.Projective.map_addX

added theorem WeierstrassCurve.Projective.map_addXYZ

added theorem WeierstrassCurve.Projective.map_addY

added theorem WeierstrassCurve.Projective.map_addZ

added theorem WeierstrassCurve.Projective.map_dblU

added theorem WeierstrassCurve.Projective.map_dblX

added theorem WeierstrassCurve.Projective.map_dblXYZ

added theorem WeierstrassCurve.Projective.map_dblY

added theorem WeierstrassCurve.Projective.map_dblZ

added theorem WeierstrassCurve.Projective.map_negAddY

added theorem WeierstrassCurve.Projective.map_negDblY

added theorem WeierstrassCurve.Projective.map_negY

added def WeierstrassCurve.Projective.negAddY

added theorem WeierstrassCurve.Projective.negAddY_eq'

added theorem WeierstrassCurve.Projective.negAddY_eq

added theorem WeierstrassCurve.Projective.negAddY_of_X_eq'

added theorem WeierstrassCurve.Projective.negAddY_of_X_eq

added theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.negAddY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.negAddY_self

added theorem WeierstrassCurve.Projective.negAddY_smul

added theorem WeierstrassCurve.Projective.negDblY_eq'

added theorem WeierstrassCurve.Projective.negDblY_eq

added theorem WeierstrassCurve.Projective.negDblY_of_Y_eq'

added theorem WeierstrassCurve.Projective.negDblY_of_Y_eq

added theorem WeierstrassCurve.Projective.negDblY_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.negDblY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.negDblY_smul

added def WeierstrassCurve.Projective.negY

added theorem WeierstrassCurve.Projective.negY_eq

added theorem WeierstrassCurve.Projective.negY_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.negY_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.negY_smul

added theorem WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY

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

added theorem WeierstrassCurve.Projective.Point.add_def

added theorem WeierstrassCurve.Projective.Point.add_point

added def WeierstrassCurve.Projective.Point.fromAffine

added theorem WeierstrassCurve.Projective.Point.fromAffine_some

added theorem WeierstrassCurve.Projective.Point.fromAffine_some_ne_zero

added theorem WeierstrassCurve.Projective.Point.fromAffine_zero

added theorem WeierstrassCurve.Projective.Point.mk_ne_zero

added theorem WeierstrassCurve.Projective.Point.mk_point

added def WeierstrassCurve.Projective.Point.neg

added theorem WeierstrassCurve.Projective.Point.neg_def

added theorem WeierstrassCurve.Projective.Point.neg_point

added theorem WeierstrassCurve.Projective.Point.toAffineLift_add

added theorem WeierstrassCurve.Projective.Point.toAffineLift_eq

added theorem WeierstrassCurve.Projective.Point.toAffineLift_neg

added theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.Point.toAffineLift_some

added theorem WeierstrassCurve.Projective.Point.toAffineLift_zero

added theorem WeierstrassCurve.Projective.Point.toAffine_add

added theorem WeierstrassCurve.Projective.Point.toAffine_neg

added theorem WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.Point.toAffine_of_equiv

added theorem WeierstrassCurve.Projective.Point.toAffine_of_singular

added theorem WeierstrassCurve.Projective.Point.toAffine_smul

added theorem WeierstrassCurve.Projective.Point.toAffine_some

added theorem WeierstrassCurve.Projective.Point.toAffine_zero

added theorem WeierstrassCurve.Projective.Point.zero_def

added theorem WeierstrassCurve.Projective.Point.zero_point

added structure WeierstrassCurve.Projective.Point

added theorem WeierstrassCurve.Projective.addMap_eq

added theorem WeierstrassCurve.Projective.addMap_of_Y_eq

added theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.addMap_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.addXYZ_neg

added theorem WeierstrassCurve.Projective.addX_neg

added theorem WeierstrassCurve.Projective.addY_neg

added theorem WeierstrassCurve.Projective.addZ_neg

added theorem WeierstrassCurve.Projective.add_equiv

added theorem WeierstrassCurve.Projective.add_of_X_ne

added theorem WeierstrassCurve.Projective.add_of_Y_eq

added theorem WeierstrassCurve.Projective.add_of_Y_ne'

added theorem WeierstrassCurve.Projective.add_of_Y_ne

added theorem WeierstrassCurve.Projective.add_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_left

added theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_right

added theorem WeierstrassCurve.Projective.add_of_eq

added theorem WeierstrassCurve.Projective.add_of_equiv

added theorem WeierstrassCurve.Projective.add_of_not_equiv

added theorem WeierstrassCurve.Projective.add_self

added theorem WeierstrassCurve.Projective.add_smul_equiv

added theorem WeierstrassCurve.Projective.add_smul_of_equiv

added theorem WeierstrassCurve.Projective.add_smul_of_not_equiv

added theorem WeierstrassCurve.Projective.baseChange_add

added theorem WeierstrassCurve.Projective.baseChange_neg

added def WeierstrassCurve.Projective.neg

added theorem WeierstrassCurve.Projective.negAddY_neg

added def WeierstrassCurve.Projective.negMap

added theorem WeierstrassCurve.Projective.negMap_eq

added theorem WeierstrassCurve.Projective.negMap_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.negMap_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.neg_X

added theorem WeierstrassCurve.Projective.neg_Y

added theorem WeierstrassCurve.Projective.neg_Z

added theorem WeierstrassCurve.Projective.neg_equiv

added theorem WeierstrassCurve.Projective.neg_of_Z_eq_zero

added theorem WeierstrassCurve.Projective.neg_of_Z_ne_zero

added theorem WeierstrassCurve.Projective.neg_smul_equiv

added theorem WeierstrassCurve.Projective.nonsingularLift_addMap

added theorem WeierstrassCurve.Projective.nonsingularLift_negMap

added theorem WeierstrassCurve.Projective.nonsingular_add

added theorem WeierstrassCurve.Projective.nonsingular_neg