Theorems · Theorem · group theory

Rep.ihom_map

∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] (A : Rep.{w, u, v} k G) {X Y : Rep.{u_1, u, v} k G}
  (f : X ⟶ Y),
  A.ihom.map f =
    Rep.ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X ↑Y) (Rep.Hom.hom f).toLinearMap, isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroup