addXYZ — Mathlib

English

The X-coordinate of the sum in addXYZ matches the X-coordinate of addX: addXYZ P Q x = addX P Q.

Русский

X-координата суммы в addXYZ совпадает с X-координатой операции addX: addXYZ P Q x = addX P Q.

LaTeX

$$$$ \\operatorname{addXYZ}(P,Q)_x = \\operatorname{addX}(P,Q) $$$$

Lean4

/-- The coordinates of a representative of `P + Q` for two distinct Jacobian 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, addZ P Q]

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