addZ_self

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Jacobian.addZ_self

English

For any P, the Z-coordinate of P added to itself vanishes: addZ(P,P) = 0.

Русский

Для любой точки P Z-координата суммы P + P равна нулю: addZ(P,P) = 0.

LaTeX

$$$\operatorname{addZ}(P,P) = 0$$$

Lean4

theorem addZ_self (P : Fin 3 → R) : addZ P P = 0 :=
  sub_self <| P x * P z ^ 2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru