Theorems · Theorem · category theory

Action.FintypeCat.quotientToEndHom_mk

∀ {G : Type u_1} [inst : Group G] (H N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] (x : ↥H) (g : G),
  (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.quotientToEndHom H N) ⟦x⟧).hom) ⟦g⟧ = ⟦g * ↑x⁻¹⟧

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFintypeSubgroup.Normal