add_of_Z_eq_zero_right — Mathlib

English

Let W' be the Jacobian, and suppose P lies on W' with P_z ≠ 0 while Q lies on W' with Q_z = 0. Then the sum W'.add P Q equals the negation of (Q_0 P_2) times P, i.e. W'.add P Q = - (Q_0 P_2) · P.

Русский

Пусть W' — якобиан; пусть P_z ≠ 0, Q_z = 0; тогда сумма W'.add P Q равна отрицательному умножению P на коэффициент (Q_0 P_2): W'.add P Q = - (Q_0 P_2) · P.

LaTeX

$$$W'.add\,P\,Q = -\,(Q_0 \cdot P_2) \cdot P$$$

Lean4

theorem add_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQ : W'.Equation Q) (hPz : P z ≠ 0) (hQz : Q z = 0) :
    W'.add P Q = -(Q x * P z) • P := by
  rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

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