Commit 2026-02-26 23:01 c31e0d01

View on Github →

feat(AlgebraicGeometry/EllipticCurve/Affine/Point): add equivalences between points and explicit WithZero types (#25984) This PR continues the work from #14627. Original PR: https://github.com/leanprover-community/mathlib4/pull/14627

Estimated changes

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

added def WeierstrassCurve.Affine.Point.mk

modified theorem WeierstrassCurve.Affine.Point.some_ne_zero

modified theorem WeierstrassCurve.Affine.Point.zero_def

added def WeierstrassCurve.Affine.nonsingularPointEquiv

added def WeierstrassCurve.Affine.nonsingularPointEquivSubtype

added theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_some

added theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_none

added theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_some

added theorem WeierstrassCurve.Affine.nonsingularPointEquivSubtype_zero

added theorem WeierstrassCurve.Affine.nonsingularPointEquiv_some

added theorem WeierstrassCurve.Affine.nonsingularPointEquiv_symm_none

added theorem WeierstrassCurve.Affine.nonsingularPointEquiv_symm_some

added theorem WeierstrassCurve.Affine.nonsingularPointEquiv_zero

added def WeierstrassCurve.Affine.pointEquiv

added def WeierstrassCurve.Affine.pointEquivSubtype

added theorem WeierstrassCurve.Affine.pointEquivSubtype_some

added theorem WeierstrassCurve.Affine.pointEquivSubtype_symm_none

added theorem WeierstrassCurve.Affine.pointEquivSubtype_symm_some

added theorem WeierstrassCurve.Affine.pointEquivSubtype_zero

added theorem WeierstrassCurve.Affine.pointEquiv_some

added theorem WeierstrassCurve.Affine.pointEquiv_symm_none

added theorem WeierstrassCurve.Affine.pointEquiv_symm_some

added theorem WeierstrassCurve.Affine.pointEquiv_zero