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.

src/group_theory/subgroup.lean

@@ -861,8 +861,8 @@ instance center_normal : (center G).normal :=
 end⟩
 
 variables {G} (H)
-/-- The `normalizer` of `H` is the smallest subgroup of `G` inside which `H` is normal. -/
-@[to_additive "The `normalizer` of `H` is the smallest subgroup of `G` inside which `H` is normal."]
+/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
+@[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."]
 def normalizer : subgroup G :=
 { carrier := {g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H},
   one_mem' := by simp,