mathlib

e489ca1d - feat(group_theory/p_group): Intersection with p-subgroup is a p-subgroup (#9189)

feat(group_theory/p_group): Intersection with p-subgroup is a p-subgroup (#9189) Two lemmas stating that the intersection with a p-subgroup is a p-subgroup. Not sure which one should be called left and which one should be called right though :)