# mathlibdocumentation

group_theory.specific_groups.dihedral

# Dihedral Groups #

We define the dihedral groups dihedral_group n, with elements r i and sr i for i : zmod n.

For n ≠ 0, dihedral_group n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. dihedral_group 0 corresponds to the infinite dihedral group.

@[protected, instance]
inductive dihedral_group (n : ) :
Type

For n ≠ 0, dihedral_group n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. dihedral_group 0 corresponds to the infinite dihedral group.

Instances for dihedral_group
@[protected, instance]
Equations
@[protected, instance]
def dihedral_group.group {n : } :

The group structure on dihedral_group n.

Equations
• dihedral_group.group = {mul := mul n, mul_assoc := _, one := one n, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5, npow_zero' := _, npow_succ' := _, inv := inv n, div := div_inv_monoid.div._default mul dihedral_group.group._proof_8 one dihedral_group.group._proof_9 dihedral_group.group._proof_10 (div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5) dihedral_group.group._proof_11 dihedral_group.group._proof_12 inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default mul dihedral_group.group._proof_14 one dihedral_group.group._proof_15 dihedral_group.group._proof_16 (div_inv_monoid.npow._default one mul dihedral_group.group._proof_4 dihedral_group.group._proof_5) dihedral_group.group._proof_17 dihedral_group.group._proof_18 inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem dihedral_group.r_mul_r {n : } (i j : zmod n) :
@[simp]
theorem dihedral_group.r_mul_sr {n : } (i j : zmod n) :
@[simp]
theorem dihedral_group.sr_mul_r {n : } (i j : zmod n) :
@[simp]
theorem dihedral_group.sr_mul_sr {n : } (i j : zmod n) :
theorem dihedral_group.one_def {n : } :
@[protected, instance]

If 0 < n, then dihedral_group n is a finite group.

Equations
@[protected, instance]
theorem dihedral_group.card {n : } [ne_zero n] :
= 2 * n

If 0 < n, then dihedral_group n has 2n elements.

@[simp]
theorem dihedral_group.r_one_pow {n : } (k : ) :
@[simp]
theorem dihedral_group.r_one_pow_n {n : } :
= 1
@[simp]
theorem dihedral_group.sr_mul_self {n : } (i : zmod n) :
@[simp]
theorem dihedral_group.order_of_sr {n : } (i : zmod n) :

If 0 < n, then sr i has order 2.

@[simp]

If 0 < n, then r 1 has order n.

theorem dihedral_group.order_of_r {n : } [ne_zero n] (i : zmod n) :
= n / n.gcd i.val

If 0 < n, then i : zmod n has order n / gcd n i.