addU — Mathlib

English

The unit u associated to the sum P+Q of two projective points on a Weierstrass curve (not 2-torsion) is u = - (P_y Q_z - Q_y P_z)^3 / (P_z Q_z).

Русский

Единица u, связанная с суммой P+Q двух точек на кривой Вейерштрасса (не двойной тождественности), задаётся как u = - (P_y Q_z - Q_y P_z)^3 / (P_z Q_z).

LaTeX

$$$\text{addU}(P,Q) = -\frac{(P_y Q_z - Q_y P_z)^3}{P_z Q_z}$$$

Lean4

/-- The unit associated to a representative of `P + Q` for two projective 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 • ![0, 1, 0]` where `P x / P z = Q x / Q z`
but `P ≠ W.neg P`. -/
def addU (P Q : Fin 3 → F) : F :=
  -(P y * Q z - Q y * P z) ^ 3 / (P z * Q z)

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