Theorems · Inductive type · group theory

Subgroup.IsSubnormal

{G : Type u_1} → [inst : Group G] → Subgroup G → Prop

A subgroup H of a group G satisfies IsSubnormal if * either H = ⊤; * or there is a subgroup K of G containing H and such that H is normal in K and K satisfies IsSubnormal. Equivalently, H.IsSubnormal means that there is a chain of subgroups H₀ ≤ H₁ ≤ ... ≤ Hₙ such that * H = H₀, * G = Hₙ, * for each i ∈ {0, ..., n - 1}, Hᵢ is a normal subgroup of Hᵢ₊₁. See isSubnormal_iff for this characterisation.

Defined in

Mathlib.GroupTheory.IsSubnormal

Cited by

19 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Group