addX_eq_addX_negY_sub — Mathlib

English

The sum of two points on a Weierstrass curve satisfies a concrete equation relating x-coordinates, y-coordinates, and the slope parameter.

Русский

Сумма двух точек на кривой Вейерштрасса удовлетворяет конкретному уравнению, связывающему координаты x, y и наклон.

LaTeX

$$W.Equation (W.addX x1 x2 (W.slope x1 x2 y1 y2)) (W.addY x1 x2 y1 (W.slope x1 x2 y1 y2))$$

Lean4

/-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`,
where `ψ(x,y) = 2y + a₁x + a₃`. -/
theorem addX_eq_addX_negY_sub {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) =
      W.addX x₁ x₂ (W.slope x₁ x₂ y₁ <| W.negY x₂ y₂) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2 :=
  by
  simp_rw [slope_of_X_ne hx, addX, negY, ← neg_sub x₁, neg_sq]
  simp [field]
  ring1
    -- see https://github.com/leanprover-community/mathlib4/issues/29041

Похожие утверждения