add_of_Y_ne — Mathlib

English

If P_z ≠ 0 and Q equations satisfy X-ne condition, then W.add P Q equals W.addZ P Q multiplied by a vector determined by the affine coordinates and slope.

Русский

Если P_z ≠ 0 и выполняются условия X ≠ на Q, то W.add P Q равно W.addZ P Q умноженному на вектор, заданный аффинными координатами и наклоном.

LaTeX

$$$ W.add P Q = W.addZ P Q \\cdot \\llbracket W.toAffine.addX (P_x/P_z) (Q_x/Q_z) (\\text{слой}) , W.toAffine.addY (P_x/P_z) (Q_x/Q_z) (P_y/P_z) (\\text{слой наклона}), 1 \\rrbracket $$$

Lean4

theorem add_of_Y_ne {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) (hy : P y * Q z ≠ Q y * P z) : W.add P Q = addU P Q • ![0, 1, 0] := by
  rw [add_of_not_equiv <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]

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