Theorem WeierstrassCurve.Jacobian.not_equiv_of_Y_ne

Modification history

2024-05-28 09:02

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

feat(AlgebraicGeometry/EllipticCurve/Jacobian): add API for equations and nonsingularity (#13060)

Added WeierstrassCurve.Jacobian.not_equiv_of_Y_ne View on Github →