addXYZ_smul — Mathlib

English

For P,Q and scalars u,v, addXYZ with (u·P) and (v·Q) equals (uv)^2 times addXYZ(P,Q): addXYZ(uP, vQ) = (uv)^2 · addXYZ(P,Q).

Русский

При масштабировании P и Q на числа u и v выполняется: addXYZ(uP, vQ) = (uv)^2 · addXYZ(P,Q).

LaTeX

$$$\mathrm{addXYZ}(u\cdot P, v\cdot Q) = (u v)^2 \cdot \mathrm{addXYZ}(P,Q)$$$

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]

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