Goal
Provide the LMFDB group label N.i — order N and the GAP small-group id i — i.e. a canonical identification of a finite group up to isomorphism.
What already exists
- mathlib: finite group theory,
Fintype.card, isomorphism (MulEquiv), and named small groups (DihedralGroup, QuaternionGroup, CyclicGroup/ZMod, Equiv.Perm/alternatingGroup). There is no small-groups catalogue / canonical labelling.
What's missing
- A decidable up-to-isomorphism identifier for small finite groups matching the GAP/LMFDB
N.i numbering (at least for small N), or a mapping from mathlib's named families to their labels.
Test cases
C_2 = 2.1, C_2² = 4.2, S_3 = 6.1, Q_8 = 8.4, D_4 = 8.3.
LMFDB targets
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Provide the LMFDB group label
N.i— orderNand the GAP small-group idi— i.e. a canonical identification of a finite group up to isomorphism.What already exists
Fintype.card, isomorphism (MulEquiv), and named small groups (DihedralGroup,QuaternionGroup,CyclicGroup/ZMod,Equiv.Perm/alternatingGroup). There is no small-groups catalogue / canonical labelling.What's missing
N.inumbering (at least for smallN), or a mapping from mathlib's named families to their labels.Test cases
C_2 = 2.1,C_2² = 4.2,S_3 = 6.1,Q_8 = 8.4,D_4 = 8.3.LMFDB targets
group.labelgroup.ordergroup.isomorphismNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.