The dihedral groups

module group-theory.dihedral-groups where

open import elementary-number-theory.groups-of-modular-arithmetic
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import group-theory.dihedral-group-construction
open import group-theory.groups

Idea

The dihedral group D_k is defined by the dihedral group construction applied to the cyclic group ℤ-Mod k.

Definition

dihedral-group : ℕ → Group lzero
dihedral-group k = dihedral-group-Ab (ℤ-Mod-Ab k)