add — Mathlib

English

If P ≈ P' and Q ≈ Q' are equivalent projective representatives, then their sums are equivalent: W'.add P Q ≈ W'.add P' Q'.

Русский

Если P ≈ P' и Q ≈ Q' — эквивалентные представления точек, то их суммы эквивалентны: W'.add P Q ≈ W'.add P' Q'.

LaTeX

$$$ W'.add P Q \\approx W'.add P' Q' $$$

Lean4

/-- The addition of two projective 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

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