English
The normal core of a subgroup H is the largest normal subgroup contained in H.
Русский
Нормальное ядро подгруппы H — наибольшая нормальная подгруппа, содержащаяся в H.
LaTeX
$$$ \mathrm{normalCore}(H) = \{ a \in G \mid \forall b \in G, b a b^{-1} \in H \} $$$
Lean4
/-- The normal core of a subgroup `H` is the largest normal subgroup of `G` contained in `H`,
as shown by `Subgroup.normalCore_eq_iSup`. -/
def normalCore (H : Subgroup G) : Subgroup G
where
carrier := {a : G | ∀ b : G, b * a * b⁻¹ ∈ H}
one_mem' a := by rw [mul_one, mul_inv_cancel]; exact H.one_mem
inv_mem' {_} h b := (congr_arg (· ∈ H) conj_inv).mp (H.inv_mem (h b))
mul_mem' {_ _} ha hb c := (congr_arg (· ∈ H) conj_mul).mp (H.mul_mem (ha c) (hb c))
