mathlib3

8aa18938 - feat(group_theory/subgroup/basic): Analog of `mul_aut.conj` for normal subgroups. (#9552)

feat(group_theory/subgroup/basic): Analog of `mul_aut.conj` for normal subgroups. (#9552) Analog of `mul_aut.conj` for normal subgroups (pretty much just copying the code from `data/equiv/mul_add_aut.lean`). Co-authored-by: tb65536 <tb65536@users.noreply.github.com>