Theorems · Theorem · group theory

Rep.tensorHomEquiv_symm_apply

∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A.ihom.obj C),
  (A.tensorHomEquiv B C).symm f =
    Rep.ofHom
      { toLinearMap := (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).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