Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quaternion_group.order_of_a_one

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) …
Modified quaternion_group.order_of_a_oneView on Github →
2021-03-18 09:41
src/group_theory/quaternion_group.lean
feat(group_theory/quaternion_group): define the (generalised) quaternion groups (#6683) …
Added quaternion_group.order_of_a_oneView on Github →