addXYZ_X

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

English

The first component of addXYZ is addX: (addXYZ P Q)_1 = addX P Q.

Русский

Первая компонентa addXYZ совпадает с addX: (addXYZ P Q)_1 = addX P Q.

LaTeX

$$$\big(\mathrm{addXYZ}(P,Q)\big)_1 = \mathrm{addX}(P,Q)$$$

Lean4

theorem addXYZ_X (P Q : Fin 3 → R) : W'.addXYZ P Q x = W'.addX P Q :=
  rfl

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

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

Разделы

Аффилиация

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