negAddY_of_X_eq' — Mathlib

English

If P and Q lie on W and P_x Q_z ≠ Q_x P_z, then negAddY(P,Q) equals a certain explicit homogeneous polynomial in the coordinates.

Русский

Если P и Q лежат на W и P_x Q_z ≠ Q_x P_z, то negAddY(P,Q) выражается конкретным однородным полиномом по координатам.

LaTeX

$$$W'.negAddY(P,Q) = \dfrac{\text{(explicit polynomial in }P_i,Q_i,a_j)}{(P_z Q_z)^2}$$$

Lean4

theorem negAddY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P x * Q z = Q x * P z) :
    W'.negAddY P Q * (P z * Q z) ^ 2 = (P y * Q z - Q y * P z) ^ 3 * (P z * Q z) :=
  by
  rw [negAddY_eq' hP hQ, hx]
  ring1

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