mathlib
22924634 - doc(group_theory): fix `normalizer` docstring (#7231)

Commit
4 years ago
doc(group_theory): fix `normalizer` docstring (#7231) The _smallest_ subgroup of `G` inside which `H` is normal is `H` itself. The _largest_ subgroup of `G` inside which `H` is normal is the normalizer. Also confirmed by Wikipedia (see the 5th bullet point under "Groups" at [the list of properties of the centralizer and normalizer](https://en.wikipedia.org/wiki/Centralizer_and_normalizer#Properties)), because it's good to have independent confirmation for something so easy to confuse.
Author
Parents
Loading