Skip to main content

FiniteGroup

typeclass G: FiniteGroup extends Group {
    elements: List[G]
    all_group_elements_in_elements(g: G) {
        G.elements.contains_every
    }
    unique_elements_list {
        G.elements.is_unique
    }
}

A group is finite if its elements can be placed in a (finite) list

GitHub

all_group_elements_in_elements​

all_group_elements_in_elements(g: G) {
    G.elements.contains_every
}

Every group element appears in the elements list.

cyclic_subgroup​

define cyclic_subgroup(self) -> FiniteSubgroup[G] {
    FiniteSubgroup.new(map(G.order.range, self.pow).unique)
}

The cyclic subgroup generated by this element.

elements​

elements: List[G]

A list containing all elements of the group.

identity_subgroup​

let identity_subgroup: FiniteSubgroup[G] = FiniteSubgroup.new(List.singleton[G](G.1))

The trivial subgroup containing only the identity element.

inverse​

Inherited from Group.

inverse_right​

Inherited from Group.

mul​

Inherited from Semigroup.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.

order​

let order: Nat = G.elements.length

The number of elements in the group.

pow​

Inherited from Monoid.

unique_elements_list​

unique_elements_list {
    G.elements.is_unique
}

The elements list contains no duplicates.