Theorems · Theorem · group theory

IsConj.normalClosure_eq_top_of

∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N} {hg' : g' ∈ N},
  IsConj g g' → Subgroup.normalClosure {⟨g, hg⟩} = ⊤ → Subgroup.normalClosure {⟨g', hg'⟩} = ⊤

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupSubgroup.Normal