endTensorEndAlgHom_apply — Mathlib

English

Applying endTensorEndAlgHom to f ⊗ g yields the map that sends (m ⊗ n) to f(m) ⊗ g(n) via AlgebraTensorModule.map.

Русский

Применение endTensorEndAlgHom к f ⊗ g даёт отображение, отправляющее m ⊗ n в соответствующее отображение через AlgebraTensorModule.map.

LaTeX

$$endTensorEndAlgHom (f ⊗ g) = AlgebraTensorModule.map f g$$

Lean4

theorem endTensorEndAlgHom_apply (f : End A M) (g : End R N) :
    endTensorEndAlgHom (R := R) (S := S) (A := A) (M := M) (N := N) (f ⊗ₜ[R] g) = AlgebraTensorModule.map f g :=
  rfl

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