mathlib

3aa57492 - feat(group_theory/subgroup/basic): Define characteristic subgroups (#9921)

feat(group_theory/subgroup/basic): Define characteristic subgroups (#9921) This PR defines characteristic subgroups and builds the basic API. Getting `@[to_additive]` to work correctly was a bit tricky, so I mostly just copied the setup for `subgroup.normal`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>