dblZ — Mathlib

English

The Z-coordinate after scaling is multiplied by u^4: W'.dblZ (u • P) = u^4 · W'.dblZ P.

Русский

Z-координата после масштабирования умножается на u^4: W'.dblZ (u • P) = u^4 · W'.dblZ P.

LaTeX

$$$ W'.dblZ (u \\cdot P) = u^4 \\cdot W'.dblZ P $$$

Lean4

/-- The `Z`-coordinate of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve. -/
def dblZ (P : Fin 3 → R) : R :=
  P z * (P y - W'.negY P) ^ 3

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