map_tmul — Mathlib

English

Naturally commutes with swapping the factors in the two arguments.

Русский

Естественно коммутирует с перестановкой факторов в двух аргументах.

LaTeX

$$$\\mathrm{map\\ f\\ g} \\circ (\\mathrm{comm}\\ R N M) = (\\mathrm{comm}\\ R Q P) \\circ \\mathrm{map\\ g\\ f}$$$

Lean4

@[simp]
theorem map_tmul (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

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