single_smul — Mathlib

English

The map single commutes with scalar multiplication: single p i (c • a) = c • single p i a.

Русский

Карта single коммутирует с умножением на скаляр: single p i (c • a) = c • single p i a.

LaTeX

$$$\text{lp.single } p i (c \cdot a) = c \cdot \text{lp.single } p i a.$$$

Lean4

@[simp]
protected theorem single_smul (p) (i : α) (c : 𝕜) (a : E i) : lp.single p i (c • a) = c • lp.single p i a :=
  ext <| Pi.single_smul _ _ _

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