English
Let W' be the Jacobian of a Weierstrass curve over a commutative ring R. For points P and Q in the three-dimensional Finite index setting, if P lies on W' with Z-coordinate equal to 0 and Q lies on W' with Z-coordinate nonzero, then their sum P ⊞ Q on the Jacobian equals the scalar multiple (P_0 Q_2) of Q, i.e. the element (P_0 Q_2) · Q.
Русский
Пусть W' является Якобианом кривой Вейерштрасса над коммутативным кольцом R. Пусть P и Q — точки соответствующего пространства; если Z-координата P равна 0, а Z-координата Q не равна 0, то сумма P + Q на Якобиане равна скалярному умножению Q на число (P_0 Q_2): (P_0 Q_2) · Q.
LaTeX
$$$W'.add\,P\,Q = (P_0 \cdot Q_2) \cdot Q$$$
Lean4
theorem add_of_Z_eq_zero_left {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) (hQz : Q z ≠ 0) :
W'.add P Q = (P x * Q z) • Q := by
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]
