add — Mathlib

English

The addition of two Jacobian point representatives is defined by a conditional: if P ≈ Q then W'.dblXYZ P else W'.addXYZ P Q.

Русский

Сложение двух представителей точки на Якобиане определяется условием: если P ≈ Q, то W'.dblXYZ P, иначе W'.addXYZ P Q.

LaTeX

$$$\mathrm{add}(P,Q) = \begin{cases} \mathrm{dblXYZ}(P) & \text{if } P \approx Q,\\[4pt] \mathrm{addXYZ}(P,Q) & \text{otherwise}. \end{cases}$$$

Lean4

/-- The addition of two Jacobian point representatives on a Weierstrass curve. -/
noncomputable def add (P Q : Fin 3 → R) : Fin 3 → R :=
  if P ≈ Q then W'.dblXYZ P else W'.addXYZ P Q

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