neg_smul — Mathlib

English

The negation operation is linear with respect to scalar multiplication: for any P and u ∈ R, W'.neg (u · P) = u · W'.neg P.

Русский

Отображение отрицания линейно по скаляру: W'.neg( u · P ) = u · W'.neg P.

LaTeX

$$$$W'.neg (u \cdot P) = u \cdot W'.neg P$$$$

Lean4

protected theorem neg_smul (P : Fin 3 → R) (u : R) : W'.neg (u • P) = u • W'.neg P := by
  simpa only [neg, negY_smul] using (smul_fin3 (W'.neg P) u).symm

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