negAddY_of_X_eq — Mathlib

English

Let P,Q be points with W.Equation P and W.Equation Q on the Weierstrass Jacobian over F, with nonzero z-coordinates (P_z ≠ 0, Q_z ≠ 0) and hx: P_x Q_z^2 = Q_x P_z^2. Then the Y-coordinate of the sum equals (−addU(P,Q))^3, i.e., W.negAddY P Q = (−addU P Q)^3.

Русский

Пусть P,Q принадлежат кривой Вейерштрасса на Якобиане над полем F, и P_z ≠ 0, Q_z ≠ 0, а hx: P_x Q_z^2 = Q_x P_z^2. Тогда Y-компонента суммы равна (−addU(P,Q))^3, то есть W.negAddY P Q = (−addU P Q)^3.

LaTeX

$$$$ W.negAddY(P,Q) = (-\\text{addU}(P,Q))^3 $$$$

Lean4

theorem negAddY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W.negAddY P Q = (-addU P Q) ^ 3 := by
  rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

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