map₂_apply_tmul — Mathlib

English

HomTensorHomMap applied to a simple tensor equals the bilinear map of the components.

Русский

При применении homTensorHomMap к простому тензору получаем билинейное отображение компонентов.

LaTeX

$$homTensorHomMap R M N P Q (f ⊗ₜ g) = map f g$$

Lean4

@[simp]
theorem map₂_apply_tmul (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) :
    map₂ f g (m ⊗ₜ n) = map (f m) (g n) :=
  rfl

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