English
A refined cross-form of addX shows a proportionality relation when the x-coordinates satisfy a linear relation; addX(P,Q) is the product of a certain polynomial with (P_x Q_z − Q_x P_z) divided by (P_z Q_z)^2.
Русский
Уточнённое соотношение addX при линейной зависимости x-координат; addX(P,Q) пропорционально полиному по координатам P,Q на (P_x Q_z − Q_x P_z)/(P_z Q_z)^2.
LaTeX
$$$W'.addX(P,Q) = \dfrac{N(P,Q)\,(P_x Q_z - Q_x P_z)}{(P_z Q_z)^2}$, где $N(P,Q)$ — соответствующий полином от координат.$$
Lean4
theorem addX_of_Z_ne_zero [DecidableEq F] {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) :
W.addX P Q / W.addZ P Q =
W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)) :=
by
rw [addX_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
toAffine_addX_of_ne hPz hQz <| sub_ne_zero.mpr hx]
