Theorems · Theorem · group theory

Subgroup.map_normalClosure

∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set G) (f : G →* N),
  Function.Surjective ⇑f → Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s)

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupGroup