addY_smul — Mathlib

English

Scaling P by u and Q by v scales addY by (u v)^6: addY(u·P, v·Q) = ( (u v)^2 )^3 · addY(P,Q).

Русский

Умножение P на скаляр u и Q на v масштабирует addY на (u v)^6: addY(u·P, v·Q) = ( (u v)^2 )^3 · addY(P,Q).

LaTeX

$$$$ \\operatorname{addY}(u\\cdot P, v\\cdot Q) = ((u v)^2)^3 \\cdot \\operatorname{addY}(P,Q) $$$$

Lean4

theorem addY_smul (P Q : Fin 3 → R) (u v : R) : W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q :=
  by
  simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_smul]
  ring1

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