Theorems · Inductive type · group theory

AddSubgroup.IsSubnormal

{G : Type u_2} → [inst : AddGroup G] → AddSubgroup G → Prop

An additive subgroup H of an additive group G satisfies IsSubnormal if * either H = ⊤; * or there is an additive 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 additive subgroups H₀ ≤ H₁ ≤ ... ≤ Hₙ such that * H = H₀, * G = Hₙ, * for each i ∈ {0, ..., n - 1}, Hᵢ is a normal additive subgroup of Hᵢ₊₁. See isSubnormal_iff for this characterisation.

Defined in

Mathlib.GroupTheory.IsSubnormal

Cited by

17 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddGroup