addXYZ_Y

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

English

The second component of addXYZ is addY: (addXYZ P Q)_2 = addY P Q.

Русский

Вторая компонентa addXYZ равна addY: (addXYZ P Q)_2 = addY P Q.

LaTeX

$$$\big(\mathrm{addXYZ}(P,Q)\big)_2 = \mathrm{addY}(P,Q)$$$

Lean4

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

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

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

Разделы

Аффилиация

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