Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.slope_of_Y_ne

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  x₁ = x₂ →
    y₁ ≠ W.negY x₂ y₂ → W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Cited by

3 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Quot.sound

Assumes

FieldDecidableEq