Theorems · Definition · group theory

AddSubgroup.IsSubnormal.below.casesOn

∀ {G : Type u_2} [inst : AddGroup G] {motive : (a : AddSubgroup G) → a.IsSubnormal → Prop}
  {motive_1 : {a : AddSubgroup G} → (t : a.IsSubnormal) → AddSubgroup.IsSubnormal.below t → Prop} {a : AddSubgroup G}
  {t : a.IsSubnormal} (t_1 : AddSubgroup.IsSubnormal.below t),
  motive_1 ⋯ ⋯ →
    (∀ (H K : AddSubgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.addSubgroupOf K).Normal)
        (ih : AddSubgroup.IsSubnormal.below hSubn) (hSubn_ih : motive K hSubn), motive_1 ⋯ ⋯) →
      motive_1 t t_1

Defined in

Mathlib.GroupTheory.IsSubnormal

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroup