linearHomEquivComm_hom — Mathlib

English

The commuted version of linearHomEquiv_hom is given by curry without flip.

Русский

Коммутированная версия linearHomEquiv_hom задаётся через curry без flip.

LaTeX

$$$$ (MonoidalClosed.linearHomEquivComm A B C f).hom = \\ModuleCat.ofHom (TensorProduct.curry f.hom.hom). $$$$

Lean4

@[simp]
theorem linearHomEquivComm_hom (f : A ⊗ B ⟶ C) :
    (MonoidalClosed.linearHomEquivComm A B C f).hom = ModuleCat.ofHom (TensorProduct.curry f.hom.hom) :=
  rfl

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