mathlib

a8a8edcb - feat(group_theory/p_group): Generalize to infinite p-groups (#9082)

feat(group_theory/p_group): Generalize to infinite p-groups (#9082) Defines p-groups, and generalizes the results of `p_group.lean` to infinite p-groups. The eventual goal is to generalize Sylow's theorems to infinite groups.