Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-18 09:41 216aecd7

View on Github →

feat(group_theory/quaternion_group): define the (generalised) quaternion groups (#6683) This PR introduces the generalised quaternion groups and determines the orders of its elements.

Estimated changes

deleted theorem dihedral.card
deleted theorem dihedral.one_def
deleted theorem dihedral.order_of_r
deleted theorem dihedral.order_of_r_one
deleted theorem dihedral.order_of_sr
deleted theorem dihedral.r_mul_r
deleted theorem dihedral.r_mul_sr
deleted theorem dihedral.r_one_pow
deleted theorem dihedral.r_one_pow_n
deleted theorem dihedral.sr_mul_r
deleted theorem dihedral.sr_mul_self
deleted theorem dihedral.sr_mul_sr
deleted inductive dihedral
added theorem dihedral_group.card
added theorem dihedral_group.one_def
added theorem dihedral_group.r_mul_r
added inductive dihedral_group