addXYZ_Y

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

The Y-coordinate of addXYZ equals the Y-coordinate of the sum: addXYZ P Q y = addY P Q.

Русский

Y-координата addXYZ совпадает с Y-координатой суммы: addXYZ P Q y = addY P Q.

LaTeX

$$$$ \\operatorname{addXYZ}(P,Q)_y = \\operatorname{addY}(P,Q) $$$$

Lean4

theorem addXYZ_Y (P Q : Fin 3 → R) : W'.addXYZ P Q y = W'.addY P Q :=
  rfl

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

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

Разделы

Аффилиация

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