Theorems · Theorem · group theory

Subgroup.le_normalizer_closure_iff

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {s : Set G},
  H ≤ Subgroup.normalizer ↑(Subgroup.closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ Subgroup.closure s

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Group