negAddY_smul — Mathlib

English

For Fin 3 → R, scaling the inputs by u and v scales the negAddY operation in a multiplicative way: W'.negAddY(u·P, v·Q) = (u v)^2)^3 · W'.negAddY(P,Q).

Русский

Для функций Fin 3 → R, умножение аргументов на u и v масштабирует операцию negAddY пропорционально: W'.negAddY(u·P, v·Q) = ((u v)^2)^3 · W'.negAddY(P,Q).

LaTeX

$$$$W'.negAddY (u \cdot P) (v \cdot Q) = \bigl((u v)^2\bigr)^3 \cdot W'.negAddY P Q.$$$$

Lean4

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

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