addXYZ_self — Mathlib

English

For any P with W'.Equation P, the sum P+P has coordinates equal to the zero vector: addXYZ_self(P) = [0,0,0].

Русский

Для любой P с W'.Equation P сумма P+P имеет координаты нулевого вектора: addXYZ_self(P) = [0,0,0].

LaTeX

$$$$ \\operatorname{addXYZ}(P,P) = [0,0,0] $$$$

Lean4

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

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