map_tmul — Mathlib

English

For Lie-module morphisms f: M →₅⁅R,L⁆ P and g: N →₅⁅R,L⁆ Q, the map respects simple tensors: map f g (m ⊗ₜ n) = f m ⊗ₜ g n.

Русский

Для морфизмов Ли-модулей f: M →₅⁅R,L⁆ P и g: N →₅⁅R,L⁆ Q композиция сохраняет простые тензоры: map f g (m ⊗ₜ n) = f m ⊗ₜ g n.

LaTeX

$$$$map\ f\ g\ (m \otimes_\surd n) = f m \otimes_\surd g n.$$$$

Lean4

@[simp]
nonrec theorem map_tmul (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  map_tmul _ _ _ _

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