addXYZ_Z

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

English

The third component of addXYZ is addZ: (addXYZ P Q)_3 = addZ P Q.

Русский

Третья компонентa addXYZ равна addZ: (addXYZ P Q)_3 = addZ P Q.

LaTeX

$$$\big(\mathrm{addXYZ}(P,Q)\big)_3 = \mathrm{addZ}(P,Q)$$$

Lean4

theorem addXYZ_Z (P Q : Fin 3 → R) : W'.addXYZ P Q z = W'.addZ P Q :=
  rfl

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

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

Разделы

Аффилиация

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