The dihedral groups

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

Created on 2022-08-04.
Last modified on 2023-03-13.

module group-theory.dihedral-groups where
Imports 
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)

Recent changes