normal_subgroupOf_iff — Mathlib

English

Let H and K be subgroups of a group G with H ≤ K. The subgroup of G consisting of elements of H that lie in K (i.e., H ∩ K) is normal in G if and only if for every h ∈ H and k ∈ K, the element k h k⁻¹ lies in H.

Русский

Пусть H и K — подгруппы группы G, причем H ≤ K. Подгруппа G, состоящая из элементов H, которые принадлежат K (то есть H ∩ K), нормальна в G тогда и только тогда, когда для всякого h ∈ H и k ∈ K, сопряжённое k h k⁻¹ лежит в H.

LaTeX

$$$ H \le K \Rightarrow (H \cap K) \trianglelefteq G \iff \forall h \in H, \forall k \in K,\ k h k^{-1} \in H $$$

Lean4

@[to_additive]
theorem normal_subgroupOf_iff {H K : Subgroup G} (hHK : H ≤ K) :
    (H.subgroupOf K).Normal ↔ ∀ h k, h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H :=
  ⟨fun hN h k hH hK => hN.conj_mem ⟨h, hHK hH⟩ hH ⟨k, hK⟩, fun hN => { conj_mem := fun h hm k => hN h.1 k.1 hm k.2 }⟩

Похожие утверждения