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
- 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). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).