addY_of_X_eq — Mathlib

English

On a Weierstrass projective curve, if P and Q satisfy W.Equation P, W.Equation Q, P z ≠ 0, Q z ≠ 0 and P x Q z = Q x P z, then the Y-coordinate of the sum equals the affine formula plugged into addU: W.addY P Q = addU P Q.

Русский

На проективной кривой Вейерштрасса, если P и Q удовлетворяют W.Equation P, W.Equation Q и P z ≠ 0, Q z ≠ 0, P x Q z = Q x P z, то y-координата суммы равна выражению через addU: W.addY P Q = addU P Q.

LaTeX

$$$W.addY(P,Q) = \mathrm{addU}(P,Q)$$$

Lean4

theorem addY_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 = Q x * P z) : W.addY P Q = addU P Q := by
  rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz, ← addY_of_X_eq' hP hQ hPz hQz hx, ←
    pow_succ', mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

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