addXYZ — Mathlib

English

The coordinates of a representative of the sum P+Q on a Weierstrass curve are exactly the triple (addX P Q, addY P Q, addZ P Q).

Русский

Координаты представителя суммы P+Q на кривой Вейерштрасса равны тройке (addX P Q, addY P Q, addZ P Q).

LaTeX

$$$\mathrm{addXYZ}(P,Q) = \begin{pmatrix} \mathrm{addX}(P,Q) \\ \mathrm{addY}(P,Q) \\ \mathrm{addZ}(P,Q) \end{pmatrix}$$$

Lean4

/-- The coordinates of a representative of `P + Q` for two distinct projective point representatives
`P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `![0, 0, 0]`. -/
noncomputable def addXYZ (P Q : Fin 3 → R) : Fin 3 → R :=
  ![W'.addX P Q, W'.addY P Q, W'.addZ P Q]

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