Theorems · Theorem · category theory

CategoryTheory.ActionCategory.curry_apply_right

∀ {X : Type u} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {H : Type u_3} [inst_2 : Group H]
  (F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)) (g : G),
  ((CategoryTheory.ActionCategory.curry F) g).right = g

Defined in

Mathlib.CategoryTheory.Action

Cited by

0 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulActionGroup