Theorems · Definition · algebraic geometry

WeierstrassCurve.Jacobian.addXYZ

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

The coordinates 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, 0, 0].

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Cited by

15 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext

Assumes

CommRing