Commit 2021-01-03 02:24 04f8fd74

View on Github →

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.

Estimated changes

Created src/group_theory/dihedral.lean

added theorem dihedral.card

added theorem dihedral.one_def

added theorem dihedral.order_of_r

added theorem dihedral.order_of_r_one

added theorem dihedral.order_of_sr

added theorem dihedral.r_mul_r

added theorem dihedral.r_mul_sr

added theorem dihedral.r_one_pow

added theorem dihedral.r_one_pow_n

added theorem dihedral.sr_mul_r

added theorem dihedral.sr_mul_self

added theorem dihedral.sr_mul_sr

added inductive dihedral