Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quaternion_group.exponent

Modification history

2022-01-01 13:55
src/group_theory/specific_groups/quaternion.lean
feat(group_theory/specific_groups/*): computes the exponents of the dihedral and generalised quaternion groups (#11166) …
Added quaternion_group.exponentView on Github →