English
Let P and Q be points on W with P nonsingular and Q nonsingular, nonzero z-coordinates, and suppose the standard cross-relations hx and hy' hold. Then P + Q is the point at infinity.
Русский
Пусть P и Q — точки на W, при этом P ненонсиглярна, Q ненонсиглярна, z-координаты не равны нулю, и выполнены условия hx и hy'. Тогда P + Q — точка бесконечности.
LaTeX
$$$ (W.Nonsingular P) \land (W.Nonsingular Q) \land (P_z \neq 0) \land (Q_z \neq 0) \land (P_x Q_z = Q_x P_z) \land (P_y Q_z = W.negY(Q) P_z) \\ \Rightarrow W.addMap P \langle Q \rangle = \langle [0,1,0] \rangle $$$
Lean4
theorem addMap_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular 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 = W.negY Q * P z) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧ :=
by
by_cases hy : P y * Q z = Q y * P z
· rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy', smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']
· rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy, smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]
