dblXYZ_smul — Mathlib

English

Scaling the input P by u scales the 2P-vector by u^4: dblXYZ(u•P) = u^4 • dblXYZ(P).

Русский

Масштабирование точки P на u даёт масштабирование вектора удвоения на u^4: dblXYZ(u•P) = u^4 • dblXYZ(P).

LaTeX

$$$W'.dblXYZ(u \cdot P) = u^4 \cdot W'.dblXYZ(P)$$$

Lean4

theorem dblXYZ_smul (P : Fin 3 → R) (u : R) : W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P := by
  rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]

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