Theorems · Theorem · group theory

QuotientGroup.quotientQuotientEquivQuotientAux_mk

∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M)
  (x : G ⧸ N), (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) x

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.NormalSubgroup.Normal