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

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

• 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
• 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).