The Normalizer/Centralizer theorem

Stream: lean4

[Albert.J]

Is lean equipped with 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) )?

[Johan Commelin]

Please don't double post.

This channel is for questions/discussions about Lean, the language.

#mathlib4 Is for questions/discussions about mathlib
Other relevant channels for this type of question are #Is there code for X? and #maths.