Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.nonsingular_negAdd

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Nonsingular x₁ y₁ →
    W.Nonsingular x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq