theorem Hex.PermGroup.Group.order_one {n : Nat} (G : Group n) : G.order = 1 ↔ ∀ (p : Perm n), Generated G.generators p → p = Perm.id n

Exact order one is equivalent to having only the identity element.

def Hex.PermGroup.Group.isTrivial {n : Nat} (G : Group n) : Bool

Equations

• G.isTrivial = decide (G.order = 1)

theorem Hex.PermGroup.Group.isTrivial_iff {n : Nat} (G : Group n) : G.isTrivial = true ↔ ∀ (p : Perm n), Generated G.generators p → p = Perm.id n