Theorems · Theorem · group theory

Subgroup.le_normalizer_map

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {N : Type u_5} [inst_1 : Group N] (f : G →* N),
  Subgroup.map f (Subgroup.normalizer ↑H) ≤ Subgroup.normalizer ↑(Subgroup.map f H)

The image of the normalizer is contained in the normalizer of the image.

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

4 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

GroupGroup