Theorems · Definition · algebraic geometry

WeierstrassCurve.Projective.addX

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

The X-coordinate 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.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Cited by

21 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

CommRing