Theorem WeierstrassCurve.Ψ_even

Modification history

2024-11-29 11:09

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers (#13786) …

Modified WeierstrassCurve.Ψ_even View on Github →

2024-06-09 22:24

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): define division polynomials (#6703)

Added WeierstrassCurve.Ψ_even View on Github →