map_tmul — Mathlib

English

For f and g as above, the tensor product morphism respects simple tensors: map f g (x ⊗ y) = f x ⊗ g y.

Русский

Для указанных выше отображений тензорного произведения отображение на тензоре тривиально сохраняет простой тензор: map f g (x ⊗ y) = f x ⊗ g y.

LaTeX

$$$\text{map } f\, g\ (x \otimes y) = f(x) \otimes g(y)$$$

Lean4

@[simp]
theorem map_tmul (f : A →ₐc[S] C) (g : B →ₐc[R] D) (x : A) (y : B) : map f g (x ⊗ₜ y) = f x ⊗ₜ g y :=
  rfl

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