addX_of_Z_eq_zero_right

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

AddX from X uses only X and Z coordinates to define the combined X coordinate.

Русский

AddX из X использует только X и Z координаты для определения X-координаты суммы.

LaTeX

$$W'.addX P Q = ( ... ) / (P z * Q z) ^ 2$$

Lean4

theorem addX_of_Z_eq_zero_right {P Q : Fin 3 → R} (hQz : Q z = 0) : W'.addX P Q = (-(Q x * P z)) ^ 2 * P x :=
  by
  rw [addX, hQz]
  ring1

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

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

Разделы

Аффилиация

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