mathlib

91824e58 - feat(group_theory/subgroup): Normal Core (#8940)

feat(group_theory/subgroup): Normal Core (#8940) Defines normal core, and proves lemmas analogous to those for normal closure. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>