normal_of_characteristic_of_normal

English

If H is normal in G and K ≤ H is characteristic in H, then the image K under the map H → G is normal in G.

Русский

Если H нормальна в G и K ≤ H характеристическая в H, тогда образ K по включению H ↪ G нормален в G.

LaTeX

$$$ (K \mapsto H)^{\ast} \text{ is Normal in } G,$ когда $K \le H \trianglelefteq G$ и $K \text{ характерна в } H$. $$

Lean4

instance normal_of_characteristic_of_normal {H : Subgroup G} [hH : H.Normal] {K : Subgroup H} [h : K.Characteristic] :
    (K.map H.subtype).Normal :=
  ⟨fun a ha b => by
    obtain ⟨a, ha, rfl⟩ := ha
    exact K.apply_coe_mem_map H.subtype ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩⟩

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