mathlib

0f6670b8 - chore(group_theory/subgroup/basic): split out some self-contained sections (#17862)

chore(group_theory/subgroup/basic): split out some self-contained sections (#17862) This is a very big file by mathlib standards at over 3000 lines. It seems helpful to reduce that by splitting some of the less fundamental definitions into their own files.