theorem Hex.PermGroup.SameGroup.derived {n : Nat} {G H : Group n} (h : SameGroup G H) : SameGroup G.derived H.derived

def Hex.PermGroup.Group.derivedAt {n : Nat} (G : Group n) : Nat → Group n

The mathematical sequence underlying the terminating derived-series algorithm. Individual terms retain the original permutation degree.

Equations

• G.derivedAt 0 = G
• G.derivedAt k.succ = (G.derivedAt k).derived

theorem Hex.PermGroup.Group.derivedAt_succ {n : Nat} (G : Group n) (k : Nat) : G.derivedAt (k + 1) = G.derived.derivedAt k

theorem Hex.PermGroup.Group.derivedAt_inside {n : Nat} (G : Group n) (k : Nat) : (G.derivedAt k).IsSubgroup G

def Hex.PermGroup.Group.IsSolvable {n : Nat} (G : Group n) : Prop

Solvability means that a term of the derived series is trivial.

Equations

• G.IsSolvable = ∃ (k : Nat), (G.derivedAt k).order = 1

theorem Hex.PermGroup.Group.solvable_of_trivial {n : Nat} (G : Group n) (h : G.order = 1) : G.IsSolvable

theorem Hex.PermGroup.Group.solvable_derived {n : Nat} (G : Group n) : G.IsSolvable ↔ G.derived.IsSolvable

theorem Hex.PermGroup.SameGroup.derivedAt {n : Nat} {G H : Group n} (h : SameGroup G H) (k : Nat) : SameGroup (G.derivedAt k) (H.derivedAt k)

theorem Hex.PermGroup.SameGroup.solvable {n : Nat} {G H : Group n} (h : SameGroup G H) : G.IsSolvable ↔ H.IsSolvable

theorem Hex.PermGroup.Group.not_solvable_of_perfect {n : Nat} (G : Group n) (h : SameGroup G.derived G) (hn : G.order ≠ 1) : ¬G.IsSolvable

A nontrivial perfect group remains unchanged throughout its derived series.