addX_of_Z_eq_zero_left — Mathlib

English

If P lies on the curve and its Z-coordinate is zero, then the X-coordinate of P+Q reduces to P_y^2 Q_z Q_x.

Русский

Если P лежит на кривой и P_z = 0, тогда X-координата суммы P+Q равна P_y^2 Q_z Q_x.

LaTeX

$$$W'.addX(P,Q) = P_y^2 \cdot Q_z \cdot Q_x$ , при $P_z = 0$.$$

Lean4

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

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