Theorem WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero

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.nonsingular_of_Z_ne_zero View on Github →