Theorems · Theorem · group theory

Rep.tensorHomEquiv_apply

∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C),
  (A.tensorHomEquiv B C) f =
    Rep.ofHom { toLinearMap := (TensorProduct.curry (Rep.Hom.hom f).toLinearMap).flip, isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Quot.sound

Assumes

CommRingGroup