Theorems · Theorem · category theory

Action.Hom.comm

∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (self : M.Hom N) (g : G),
  CategoryTheory.CategoryStruct.comp (M.ρ g) self.hom = CategoryTheory.CategoryStruct.comp self.hom (N.ρ g)

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

7 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryMonoid