Def WeierstrassCurve.Affine.Point.mk

Modification history

2026-02-26 23:01
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
feat(AlgebraicGeometry/EllipticCurve/Affine/Point): add equivalences between points and explicit WithZero types (#25984) …
Added WeierstrassCurve.Affine.Point.mkView on Github →
2025-05-07 05:50
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
chore(AlgebraicGeometry/EllipticCurve/Affine/*): split affine files (#21356) …
Deleted WeierstrassCurve.Affine.Point.mkView on Github →
2024-11-29 22:48
Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve` (#18531) …
Added WeierstrassCurve.Affine.Point.mkView on Github →