The dihedral groups

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-08-04.
Last modified on 2023-10-09.

module group-theory.dihedral-groups where
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.standard-cyclic-groups

open import foundation.universe-levels

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


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


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

Recent changes