map_smul_right — Mathlib

English

Scaling on the left commutes with tensor-product mapping: map (r • f) g = r • map f g.

Русский

Умножение слева на отображение совместимо с отображением тензорного произведения: map (r • f) g = r • map f g.

LaTeX

$$$\\operatorname{map}(r \\cdot f, g) = r \\cdot \\operatorname{map}(f, g)$$$

Lean4

theorem map_smul_right (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g :=
  by
  ext
  simp only [compr₂_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

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