linearHomEquiv_symm_hom — Mathlib

English

The symmetric version of linearHomEquiv_hom is given by the symmetric form.

Русский

Симметричная версия linearHomEquiv_hom задаётся симметричной формой.

LaTeX

$$$$ (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).flip $$$$

Lean4

theorem linearHomEquiv_symm_hom (f : B ⟶ A ⟶[Rep k G] C) :
    ((MonoidalClosed.linearHomEquiv A B C).symm f).hom =
      ModuleCat.ofHom (TensorProduct.uncurry k A B C f.hom.hom.flip) :=
  by
  simp [linearHomEquiv]
  rfl

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