addXYZ_self

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

English

If a single point P is added to itself in 3D projective coordinates, the result is the zero vector: addXYZ(P,P) = [0,0,0].

Русский

Если сложить точку P самa с собой, результат — нулевой вектор: addXYZ(P,P) = [0,0,0].

LaTeX

$$$\mathrm{addXYZ}(P,P) = \begin{pmatrix}0\\0\\0\end{pmatrix}$$$

Lean4

theorem addXYZ_self (P : Fin 3 → R) : W'.addXYZ P P = ![0, 0, 0] := by rw [addXYZ, addX_self, addY_self, addZ_self]

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

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

Разделы

Аффилиация

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