Theorems · Inductive type · group theory
DihedralGroup
ℕ → Type
For n ≠ 0, DihedralGroup 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. DihedralGroup 0 corresponds to the infinite dihedral group.
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by56
Results whose statement or proof uses this declaration.
- DihedralGroup.Productproof · cited by 3
- DihedralGroup.equivSumstatement and proof · cited by 3
- DihedralGroup.nat_cardstatement · cited by 3
- DihedralGroup.oddCommuteEquivstatement and proof · cited by 3
- DihedralGroup.r_powstatement and proof · cited by 3
- DihedralGroup.cardstatement · cited by 2
- DihedralGroup.casesOnstatement and proof · cited by 2
- DihedralGroup.not_commutativestatement and proof · cited by 2
- DihedralGroup.orderOf_r_onestatement and proof · cited by 2
- DihedralGroup.r_one_powstatement · cited by 2
- DihedralGroup.r.injstatement · cited by 2
- DihedralGroup.r.noConfusionstatement · cited by 2