Theorem WeierstrassCurve.Jacobian.map_dblX

Modification history

2024-08-08 20:12

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

perf(Data.Nat.Cast.Basic): de-simp theorem with weak keys (#15626) …

Modified WeierstrassCurve.Jacobian.map_dblX View on Github →

2024-06-26 12:03

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

feat(EllipticCurve): lemmas in Jacobian coordinates (#13846) …

Added WeierstrassCurve.Jacobian.map_dblX View on Github →