linearHomEquivComm_symm_hom — Mathlib

English

Symm version of linearHomEquiv_symm_hom expresses the uncurry form.

Русский

Симметричная версия выражает uncurry-форму.

LaTeX

$$$$ (Rep.MonoidalClosed.linearHomEquiv A B C).symm f).hom = ModuleCat.ofHom (TensorProduct.uncurry k A.V.carrier B.V.carrier C.V.carrier f.hom.hom) $$$$

Lean4

theorem linearHomEquivComm_symm_hom (f : A ⟶ B ⟶[Rep k G] C) :
    ((MonoidalClosed.linearHomEquivComm A B C).symm f).hom =
      ModuleCat.ofHom (TensorProduct.uncurry k A B C f.hom.hom) :=
  ModuleCat.hom_ext <| TensorProduct.ext' fun _ _ => rfl

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