Theorems · Theorem · category theory

Action.FintypeCat.toEndHom_trivial_of_mem

∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] {n : G},
  n ∈ N →
    (Action.FintypeCat.toEndHom N) n =
      CategoryTheory.CategoryStruct.id (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFintypeSubgroup.Normal