Theorems · Theorem · category theory

Action.FintypeCat.quotientToQuotientOfLE_hom_mk

∀ {G : Type u_1} [inst : Group G] (H N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : Fintype (G ⧸ H)] (h : N ≤ H)
  (x : G), (CategoryTheory.ConcreteCategory.hom (Action.FintypeCat.quotientToQuotientOfLE H N h).hom) ⟦x⟧ = ⟦x⟧

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFintypeFintype