group_theory.specific_groups

Stream: general

[Julian Külshammer]

I was wondering whether it would make sense to create a subfolder of group_theory analogous to the special_functions subfolder of analysis, that is called something like specific_groups and contains facts about certain well-known groups (like the ATLAS of finite simple groups, but not restricted to simple groups). So far, I could see the second half of order_of_element which deals with cyclic groups being there, but also dihedral_group and quaternion_group. One could also think about migrating some groups from other folders like special_linear_group but that is maybe more controversial. What do you think?

[Johan Commelin]

I think it's a good idea.

[Johan Commelin]

I would live the "linear algebra" groups where they are. But all the specific finite groups could certainly go there.

[Johan Commelin]

Like, I think we just got a definition of the alternating group recently

[Aaron Anderson]

Johan Commelin said:

Like, I think we just got a definition of the alternating group recently

Almost... #6913

[Julian Külshammer]

Created in #7018 (still have to fix the imports). I interpret Johan's reply in the way that perm and free_group should also not be migrated into that folder.

[Johan Commelin]

perm is somewhat on the border. But I would leave it where it is for now. We can always move it later.

[Aaron Anderson]

The alternating group is now in mathlib. My current inclination is to leave the basic definition in group_theory/perm/sign, but we're going to want to create specific_groups/alternating_group sooner or later, because the proof of simplicity is too complicated to leave in group_theory/perm/cycle.