theorem Hex.PermGroup.Group.isSubgroup_spec {n : ℕ} (H G : Group n) : H.isSubgroup G = true ↔ closure H.generators ≤ closure G.generators

theorem Hex.PermGroup.Group.sameGroup_spec {n : ℕ} (G H : Group n) : G.sameGroup H = true ↔ closure G.generators = closure H.generators

theorem Hex.PermGroup.Group.join_spec {n : ℕ} (G H : Group n) : closure (G.join H).generators = closure G.generators ⊔ closure H.generators

theorem Hex.PermGroup.Group.orbit_spec {n : ℕ} (G : Group n) (a b : Fin n) : b ∈ G.orbit a ↔ ∃ e ∈ closure G.generators, e a = b

theorem Hex.PermGroup.Group.orbits_spec {n : ℕ} (G : Group n) (a b : Fin n) : (∃ points ∈ G.orbits, a ∈ points ∧ b ∈ points) ↔ ∃ e ∈ closure G.generators, e a = b

theorem Hex.PermGroup.Group.stabilizer_spec {n : ℕ} (G : Group n) (a : Fin n) : closure (G.stabilizer a).generators = closure G.generators ⊓ MulAction.stabilizer (Equiv.Perm (Fin n)) a

theorem Hex.PermGroup.Group.pointwise_spec {n : ℕ} (G : Group n) (points : List (Fin n)) (e : Equiv.Perm (Fin n)) : e ∈ closure (G.pointwise points).generators ↔ e ∈ closure G.generators ∧ ∀ a ∈ points, e a = a

theorem Hex.PermGroup.Group.conjugate_spec {n : ℕ} (p : Perm n) (G : Group n) (e : Equiv.Perm (Fin n)) : e ∈ closure (conjugate p G).generators ↔ p.toEquiv⁻¹ * e * p.toEquiv ∈ closure G.generators

theorem Hex.PermGroup.Group.isAbelian_spec {n : ℕ} (G : Group n) : G.isAbelian = true ↔ ∀ (p q : ↥(closure G.generators)), p * q = q * p

theorem Hex.PermGroup.Group.isNormal_spec {n : ℕ} (H G : Group n) (h : H.IsSubgroup G) : H.isNormal G h = true ↔ ((closure H.generators).subgroupOf (closure G.generators)).Normal

theorem Hex.PermGroup.Group.isTransitive_spec {n : ℕ} (G : Group n) : G.isTransitive = true ↔ 0 < n ∧ ∀ (a b : Fin n), ∃ (e : ↥(closure G.generators)), ↑e a = b