Theorems · Theorem · category theory

Action.FintypeCat.quotientToQuotientOfLE.congr_simp

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

Defined in

Mathlib.CategoryTheory.Galois.EssSurj

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupFintypeFintype