Theorems · Theorem · algebraic geometry

WeierstrassCurve.Projective.add_of_Y_eq

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W.negY Q * P 2 → W.add P Q = W.dblU P • ![0, 1, 0]

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Cited by

3 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field