Theorems · Theorem · group theory

Rep.comp_smul

∀ {k : Type u} {G : Type v} [inst : CommSemiring k] [inst_1 : Monoid G] {M N O : Rep.{u_1, u, v} k G} (f : M ⟶ N)
  (r : k) (g : N ⟶ O), CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringMonoid