dblXYZ — Mathlib

English

The coordinates of a representative of 2·P for a projective point P on a Weierstrass curve are assembled into a 3-vector by stacking the three coordinate functions: [dblX P, dblY P, dblZ P].

Русский

Координаты представителя точки 2·P на проективной кривой Вейершстрасса упакованы в вектор из трёх координат: [dblX P, dblY P, dblZ P].

LaTeX

$$$\text{dblXYZ}(P) = \Big( W'.dblX(P),\; W'.dblY(P),\; W'.dblZ(P) \Big)$$$

Lean4

/-- The coordinates of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve. -/
noncomputable def dblXYZ (P : Fin 3 → R) : Fin 3 → R :=
  ![W'.dblX P, W'.dblY P, W'.dblZ P]

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