negAddY_of_X_eq — Mathlib

English

Under the condition P_x Q_z = Q_x P_z, negAddY(P,Q) equals −addU(P,Q) up to a scalar normalization given by a3, a1, a2, etc.

Русский

При условии P_x Q_z = Q_x P_z, negAddY(P,Q) равна −addU(P,Q) с нормализацией, зависящей от коэффициентов a_i.

LaTeX

$$$W'.negAddY(P,Q) = -addU(P,Q)$ under $P_x Q_z = Q_x P_z$ (up to normalization).$$

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 = Q x * P z) : W.negAddY P Q = -addU P Q := by
  rw [addU, neg_div, neg_neg, ← mul_div_mul_right _ _ <| mul_ne_zero hPz hQz, ← negAddY_of_X_eq' hP hQ hx, ← sq,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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