negAddY_of_Z_eq_zero_right — Mathlib

English

If Q lies on W and Q_z = 0, then negAddY(P,Q) equals −(Q_y^2 P_z) P_x (mod coefficients).

Русский

Если Qz = 0, то negAddY(P,Q) = −(Q_y^2 P_z) P_x (с учетом коэффициентов).

LaTeX

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

Lean4

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

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