mathlib
04f8fd74 - feat(group_theory/dihedral): add dihedral groups (#5171)

Commit
5 years ago
feat(group_theory/dihedral): add dihedral groups (#5171) Contains a subset of the content of #1076 , but implemented slightly differently. In #1076, finite and infinite dihedral groups are implemented separately, but a side effect of what I did was that `dihedral 0` corresponds to the infinite dihedral group. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Parents
Loading