addU — Mathlib

English

If P_z = 0 then addU(P, Q) = 0.

Русский

Если P_z = 0, то addU(P, Q) = 0.

LaTeX

$$$P_z = 0 \\Rightarrow \\mathrm{addU}(P,Q) = 0$$$

Lean4

/-- The unit associated to a representative of `P + Q` for two Jacobian point representatives `P`
and `Q` on a Weierstrass curve `W` that are not `2`-torsion.

More specifically, the unit `u` such that `W.add P Q = u • ![1, 1, 0]` where
`P x / P z ^ 2 = Q x / Q z ^ 2` but `P ≠ W.neg P`. -/
def addU (P Q : Fin 3 → F) : F :=
  -((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z))

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