Theorems · Theorem · algebraic geometry

WeierstrassCurve.Projective.dblX_eq

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      W.dblX P =
        ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) -
                W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 -
              2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2) *
            (P 1 - W.negY P) /
          P 2

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field