Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.derivative_addPolynomial_slope

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        Polynomial.derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) =
          -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) +
                (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) +
              (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq