Theorems · Definition · algebraic geometry

WeierstrassCurve.Jacobian.addX

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

The X-coordinate of a representative of P + Q for two distinct Jacobian point representatives P and Q on a Weierstrass curve. If the representatives of P and Q are equal, then this returns the value 0.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Cited by

25 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

CommRing