Theorems · Definition · algebraic geometry

WeierstrassCurve.Projective.addXYZ

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

The coordinates of a representative of P + Q for two distinct projective 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.Projective.Formula

Cited by

15 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext

Assumes

CommRing