Theorem WeierstrassCurve.Jacobian.addU_smul

Modification history

2026-10-31 22:39
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean
chore: remove straightforward redundant theorem hypotheses (#45526) …
Modified WeierstrassCurve.Jacobian.addU_smulView on Github →
2025-03-05 17:37
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
chore(AlgebraicGeometry/EllipticCurve/Jacobian/*): split Jacobian files (#22545)
Modified WeierstrassCurve.Jacobian.addU_smulView on Github →
2024-06-06 07:00
Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on point representatives for Jacobian coordinates (#9435) …
Added WeierstrassCurve.Jacobian.addU_smulView on Github →