add_point — Mathlib

English

Let W be the Jacobian of a Weierstrass curve. For any two points P, Q in W, the point of their sum equals the image of their coordinates under the addition map: (P + Q).point = W.addMap P.point Q.point.

Русский

Пусть W — джакобиан кривой Вейерштрасса. Для любых двух точек P и Q на W точка суммы равна образу координат этих точек под операцией сложения: (P + Q).point = W.addMap P.point Q.point.

LaTeX

$$$ (P + Q).point = W.addMap\\;P.point\\;Q.point $$$

Lean4

theorem add_point (P Q : W.Point) : (P + Q).point = W.addMap P.point Q.point :=
  rfl

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