Commit 2025-03-04 13:59 92169eb4

View on Github →

chore(AlgebraicGeometry/EllipticCurve/*): improve some proofs (#22524) This update cleans up some proofs in the Jacobian and projective coordinate files:

remove some erws and linear_combination'
replace explicit add rewrites with the existing lemma add_of(_not)_equiv
change open Classical with open scoped Classical
add mk_ne_zero to simplify the proof of fromAffine_ne_zero
extract common variables in the map and baseChange lemmas

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

modified theorem WeierstrassCurve.Jacobian.Equation.map

deleted theorem WeierstrassCurve.Jacobian.Point.fromAffine_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.fromAffine_some_ne_zero

added theorem WeierstrassCurve.Jacobian.Point.mk_ne_zero

modified theorem WeierstrassCurve.Jacobian.baseChange_add

modified theorem WeierstrassCurve.Jacobian.baseChange_addX

modified theorem WeierstrassCurve.Jacobian.baseChange_addXYZ

modified theorem WeierstrassCurve.Jacobian.baseChange_addY

modified theorem WeierstrassCurve.Jacobian.baseChange_dblU

modified theorem WeierstrassCurve.Jacobian.baseChange_dblX

modified theorem WeierstrassCurve.Jacobian.baseChange_dblXYZ

modified theorem WeierstrassCurve.Jacobian.baseChange_dblY

modified theorem WeierstrassCurve.Jacobian.baseChange_dblZ

modified theorem WeierstrassCurve.Jacobian.baseChange_equation

modified theorem WeierstrassCurve.Jacobian.baseChange_neg

modified theorem WeierstrassCurve.Jacobian.baseChange_negAddY

modified theorem WeierstrassCurve.Jacobian.baseChange_negDblY

modified theorem WeierstrassCurve.Jacobian.baseChange_negY

modified theorem WeierstrassCurve.Jacobian.baseChange_nonsingular

modified theorem WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq'

modified 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

modified theorem WeierstrassCurve.Jacobian.map_equation

modified theorem WeierstrassCurve.Jacobian.map_negAddY

modified theorem WeierstrassCurve.Jacobian.map_negDblY

modified theorem WeierstrassCurve.Jacobian.map_negY

modified theorem WeierstrassCurve.Jacobian.map_nonsingular

deleted theorem WeierstrassCurve.Jacobian.neg_smul

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

modified theorem WeierstrassCurve.Projective.Equation.map

deleted theorem WeierstrassCurve.Projective.Point.fromAffine_ne_zero

added theorem WeierstrassCurve.Projective.Point.fromAffine_some_ne_zero

added theorem WeierstrassCurve.Projective.Point.mk_ne_zero

modified theorem WeierstrassCurve.Projective.baseChange_add

modified theorem WeierstrassCurve.Projective.baseChange_addX

modified theorem WeierstrassCurve.Projective.baseChange_addXYZ

modified theorem WeierstrassCurve.Projective.baseChange_addY

modified theorem WeierstrassCurve.Projective.baseChange_dblU

modified theorem WeierstrassCurve.Projective.baseChange_dblX

modified theorem WeierstrassCurve.Projective.baseChange_dblXYZ

modified theorem WeierstrassCurve.Projective.baseChange_dblY

modified theorem WeierstrassCurve.Projective.baseChange_dblZ

modified theorem WeierstrassCurve.Projective.baseChange_equation

modified theorem WeierstrassCurve.Projective.baseChange_neg

modified theorem WeierstrassCurve.Projective.baseChange_negAddY

modified theorem WeierstrassCurve.Projective.baseChange_negDblY

modified theorem WeierstrassCurve.Projective.baseChange_negY

modified theorem WeierstrassCurve.Projective.baseChange_nonsingular

modified theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq'

modified theorem WeierstrassCurve.Projective.map_addU

modified theorem WeierstrassCurve.Projective.map_addX

modified theorem WeierstrassCurve.Projective.map_addXYZ

modified theorem WeierstrassCurve.Projective.map_addY

modified theorem WeierstrassCurve.Projective.map_addZ

modified theorem WeierstrassCurve.Projective.map_dblU

modified theorem WeierstrassCurve.Projective.map_dblX

modified theorem WeierstrassCurve.Projective.map_dblXYZ

modified theorem WeierstrassCurve.Projective.map_dblY

modified theorem WeierstrassCurve.Projective.map_dblZ

modified theorem WeierstrassCurve.Projective.map_equation

modified theorem WeierstrassCurve.Projective.map_negAddY

modified theorem WeierstrassCurve.Projective.map_negDblY

modified theorem WeierstrassCurve.Projective.map_negY

modified theorem WeierstrassCurve.Projective.map_nonsingular

deleted theorem WeierstrassCurve.Projective.neg_smul