Generating sets of groups

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-06-08.
Last modified on 2023-06-08.

module group-theory.generating-sets-groups where
Imports 
open import foundation.universe-levels

open import group-theory.full-subgroups
open import group-theory.groups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.subsets-groups

Idea

A generating set of a group G is a subset S ⊆ G such that the subgroup generated by S is the full subgroup.

Definition

The predicate of being a generating set

module _
  {l1 l2 : Level} (G : Group l1) (S : subset-Group l2 G)
  where

  is-generating-set-Group : UU (l1 ⊔ l2)
  is-generating-set-Group = is-full-Subgroup G (subgroup-subset-Group G S)

Recent changes