English
Let W be a Weierstrass projective curve over a field F. For two projective points P and Q on W, represented by triples P = (P0, P1, P2) and Q = (Q0, Q1, Q2) in Fin(3) → F, if P and Q satisfy the curve equation and P0 Q2 ≠ Q0 P2, then the Z-coordinate of their sum is a unit, i.e. W.addZ(P, Q) is invertible in F.
Русский
Пусть W — кривая Вейершрастa в проективном виде над полем F. Пусть P и Q — две точки на W, заданные тройками P = (P0, P1, P2) и Q = (Q0, Q1, Q2) в Fin(3) → F, удовлетворяющие уравнению кривой и таким условием P0 Q2 ≠ Q0 P2. Тогда Z-координата их суммы не равна нулю, то есть W.addZ(P, Q) является единицей в F.
LaTeX
$$$W.addZ(P,Q) \in F^{\times}$ provided $W.Equation(P)$, $W.Equation(Q)$ and $P_0 Q_2 \neq Q_0 P_2$.$$
Lean4
theorem isUnit_addZ_of_X_ne {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hx : P x * Q z ≠ Q x * P z) :
IsUnit <| W.addZ P Q :=
(addZ_ne_zero_of_X_ne hP hQ hx).isUnit
