Theorems · Theorem · group theory

normalizerCondition_iff_only_full_group_self_normalizing

∀ {G : Type u_1} [inst : Group G], NormalizerCondition G ↔ ∀ (H : Subgroup G), Subgroup.normalizer ↑H = H → H = ⊤

Alternative phrasing of the normalizer condition: Only the full group is self-normalizing. This may be easier to work with, as it avoids inequalities and negations.

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

Group