mathlib documentation

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.

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.

@[instance]

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 := _, gpow := div_inv_monoid.gpow._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, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}
@[simp]
@[instance]

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

Equations
theorem dihedral_group.card {n : } [fact (0 < n)] :

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

@[simp]
@[simp]
@[simp]

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 : } [fact (0 < n)] (i : zmod n) :

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