theorem Hex.PermGroup.Group.order_one_spec {n : ℕ} (G : Group n) : G.order = 1 ↔ closure G.generators = ⊥

theorem Hex.PermGroup.Group.derivedAt_spec {n : ℕ} (G : Group n) (k : ℕ) : closure (G.derivedAt k).generators = Subgroup.map (closure G.generators).subtype (_root_.derivedSeries (↥(closure G.generators)) k)

Every computational series term is the image of the corresponding Mathlib derived-series subgroup under the ambient inclusion.

theorem Hex.PermGroup.Group.solvable_spec {n : ℕ} (G : Group n) : G.IsSolvable ↔ _root_.Group.IsSolvable ↥(closure G.generators)

Solvability of the executable group is exactly Mathlib solvability of its generated subgroup; negative certificates therefore prove nonsolvability.

theorem Hex.PermGroup.Group.isSolvable_spec {n : ℕ} (G : Group n) : G.isSolvable = true ↔ _root_.Group.IsSolvable ↥(closure G.generators)