Theorems · Definition · algebraic geometry

WeierstrassCurve.Jacobian.dblU

{R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R

The unit associated to a representative of 2 • P for a Jacobian point representative P on a Weierstrass curve W that is 2-torsion. More specifically, the unit u such that W.add P P = u • ![1, 1, 0] where P = W.neg P.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Cited by

19 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing