addY_self

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

The Y-coordinate of P added to itself vanishes: addY_self(P) = 0 for any P with W'.Equation P.

Русский

Y-координата суммы точки с самой собой равна нулю: addY_self(P) = 0 при W'.Equation P.

LaTeX

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

Lean4

theorem addY_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P P = 0 :=
  by
  rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]
  ring1

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

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

Разделы

Аффилиация

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