Theorems · Definition · group theory

Subgroup.IsSubnormal.casesOn

∀ {G : Type u_1} [inst : Group G] {motive : (a : Subgroup G) → a.IsSubnormal → Prop} {a : Subgroup G}
  (t : a.IsSubnormal),
  motive ⊤ ⋯ →
    (∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal), motive H ⋯) →
      motive a t

Defined in

Mathlib.GroupTheory.IsSubnormal

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group