addY_of_Z_eq_zero_left — Mathlib

English

If P,Q lie on the curve and P_x Q_z^2 = Q_x P_z^2, then W'.addY P Q relates to −addU(P,Q) by a cubic power: W'.addY P Q · (P_z Q_z)^3 = (−addU(P,Q))^3.

Русский

Если P и Q лежат на кривой и P_x Q_z^2 = Q_x P_z^2, то W'.addY P Q пропорциональна (−addU(P,Q))^3 с коэффициентом (P_z Q_z)^3.

LaTeX

$$$$ W'.\\operatorname{addY}(P,Q) \\cdot (P_z Q_z)^3 = (-\\operatorname{addU}(P,Q))^3 $$$$

Lean4

theorem addY_of_Z_eq_zero_left {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.addY P Q = (P x * Q z) ^ 3 * Q y :=
  by
  rw [addY, negY_eq, negAddY_of_Z_eq_zero_left hP hPz, negY, addX_of_Z_eq_zero_left hPz, addZ_of_Z_eq_zero_left hPz]
  ring1

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