def Hex.PermGroup.Group.adjoin {n : Nat} (H : Group n) (p : Perm n) : Group n

Append one generator and rebuild the complete checked chain. Callers can omit redundant insertions using a complete membership test first.

Equations

• H.adjoin p = Hex.PermGroup.Group.ofGenerators (H.generators.push p)

theorem Hex.PermGroup.Group.subgroup_adjoin {n : Nat} (H : Group n) (p : Perm n) : H.IsSubgroup (H.adjoin p)

theorem Hex.PermGroup.Group.mem_adjoin {n : Nat} (H : Group n) (p : Perm n) : Generated (H.adjoin p).generators p

theorem Hex.PermGroup.Group.adjoin_le {n : Nat} (H K : Group n) (p : Perm n) : (H.adjoin p).IsSubgroup K ↔ H.IsSubgroup K ∧ Generated K.generators p

Adjoining a generator is the least subgroup containing the old group and that generator.

theorem Hex.PermGroup.Group.order_adjoin {n : Nat} (H : Group n) (p : Perm n) (hp : ¬Generated H.generators p) : 2 * H.order ≤ (H.adjoin p).order