mathlib3 documentation

group_theory.specific_groups.dihedral

Dihedral Groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ) :

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]

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 := _}
@[protected, instance]

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

Equations
@[protected, instance]

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

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

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