addXYZ_smul — Mathlib

English

Under hx and nonzero z for P,Q, the full expression for addXYZ is obtained as a product of addZ and an explicit 3-vector of affine coordinates, same structure as the previous variant.

Русский

При hx и ненулевых z-координатах P,Q выражение addXYZ получается как произведение addZ на явный 3-мерный вектор афинных координат.

LaTeX

$$$$ \\operatorname{addXYZ}(P,Q) = \\operatorname{addZ}(P,Q) \\cdot \\!\\left[ W'.toAffine.addX(\\cdots), W'.toAffine.addY(\\cdots), 1 \\right] $$$$

Lean4

theorem addXYZ_smul (P Q : Fin 3 → R) (u v : R) : W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q := by
  rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

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