The dihedral groups

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

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

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

Idea

The dihedral group Dₖ 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