tensorHom_tmul — Mathlib

English

The tensor product morphism distributes over tmul: (f ⊗ g) acting on k ⊗ m equals f k ⊗ g m.

Русский

Гомоморфизм тензорного произведения распределяется по tmul: (f ⊗ g) применяя к (k ⊗ m) даёт f(k) ⊗ g(m).

LaTeX

$$$ (f \\otimes g)(k \\otimes m) = f(k) \\otimes g(m) $$$

Lean4

@[simp]
theorem tensorHom_tmul {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
    (f ⊗ₘ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
  rfl

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