mathlib3

eaec1dae - feat(group_theory/group_action/conj_act): A characteristic subgroup of a normal subgroup is normal (#9992)

feat(group_theory/group_action/conj_act): A characteristic subgroup of a normal subgroup is normal (#9992) Uses `mul_aut.conj_normal` to prove an instance stating that a characteristic subgroup of a normal subgroup is normal.