negAddY_of_Z_eq_zero_left — Mathlib

English

If P lies on W and P_z = 0, then negAddY(P,Q) equals P_y^2 Q_z Q_x (up to coefficients).

Русский

Если Pz = 0, то negAddY(P,Q) равна выражению P_y^2 Q_z Q_x с учётом коэффициентов кривой.

LaTeX

$$$W'.negAddY(P,Q) = P_y^2 Q_z Q_x \quad\text{при } P_z=0$$$

Lean4

theorem negAddY_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q :=
  by
  rw [negAddY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, negY]
  ring1

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