The Normalizer/Centralizer theorem

Stream: mathlib4

[Albert.J]

Does mathlib have the N/C theorem (For subgroup H of G, the quotient group of the normalizer of H by the centralizer of H is isomorphic to a subgroup of Aut(H) )? I tried to search for it but didn't find any.

[Kevin Buzzard]

That's not a theorem, it's a definition and a theorem. You don't just want the claim that some group is abstractly isomorphic to a subgroup of another group, you want the actual map and then a proof that it's injective. I can believe that it's not there, but it wouldn't be hard to define.

[Thomas Browning]

Yeah, I don't think we have it yet, but it shouldn't be too hard.