Theorems · Theorem · group theory

Rep.ActionToRep_map

∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {X Y : Action (ModuleCat k) G} (f : X ⟶ Y),
  (Rep.ActionToRep k G).map f = Rep.ofHom { toLinearMap := ModuleCat.Hom.hom f.hom, isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingMonoid