dblZ — Mathlib

English

If P and Q lie on the curve with P_y = W.negY P and Hy' relation, dblZ P is constrained accordingly.

Русский

Если P и Q лежат на кривой, P_y = W.negY P и связь Hy’ ограничивают dblZ P соответствующим образом.

LaTeX

$$$P_y = W.negY P,\ Q_y = W.negY Q \Rightarrow W'.dblZ P \text{ satisfies a relation with } Q$$$

Lean4

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

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