prod_normal — Mathlib

English

If H is normal in G and K is normal in N, then the product subgroup H × K is normal in G × N.

Русский

Если H нормальна в G, а K нормальна в N, то произведение подгрупп H × K нормально в G × N.

LaTeX

$$$H \triangleleft G \land K \triangleleft N \Rightarrow H \times K \trianglelefteq G \times N$$$

Lean4

@[to_additive prod_normal]
instance prod_normal (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal where
  conj_mem n hg
    g := ⟨hH.conj_mem n.fst (Subgroup.mem_prod.mp hg).1 g.fst, hK.conj_mem n.snd (Subgroup.mem_prod.mp hg).2 g.snd⟩

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