Theorems · Definition · algebraic geometry

WeierstrassCurve.Projective.addY

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

The Y-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

19 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext

Assumes

CommRing