dualTensorIsoLinHom_hom_hom — Mathlib

English

The natural isomorphism between dual-tensor construction and Hom in the FDRep setting identifies the forward map with the canonical dualTensorHom map.

Русский

Естественное изоморождение между конструкциями двойного тензора и Hom в контексте FDRep совпадает с каноническим отображением dualTensorHom.

LaTeX

$$$(dualTensorIsoLinHom \ ρ_V\ W).hom.hom = ModuleCat.ofHom (dualTensorHom k V W)$$$

Lean4

@[simp]
theorem dualTensorIsoLinHom_hom_hom : (dualTensorIsoLinHom ρV W).hom.hom = ModuleCat.ofHom (dualTensorHom k V W) :=
  rfl

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