prod_subgroupOf_prod_normal — Mathlib

English

If H1 ≤ K1 and H2 ≤ K2 with H1 ⊲ K1 and H2 ⊲ K2, then (H1 × H2) ⊲ (K1 × K2).

Русский

Если H1 ≤ K1 и H2 ≤ K2 и H1 нормальна в K1, а H2 нормальна в K2, то H1 × H2 нормальна в K1 × K2.

LaTeX

$$$(H_1 \triangleleft K_1) \land (H_2 \triangleleft K_2) \Rightarrow (H_1 \times H_2) \trianglelefteq (K_1 \times K_2)$$$

Lean4

@[to_additive prod_addSubgroupOf_prod_normal]
instance prod_subgroupOf_prod_normal {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N} [h₁ : (H₁.subgroupOf K₁).Normal]
    [h₂ : (H₂.subgroupOf K₂).Normal] : ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal where
  conj_mem n hgHK
    g :=
    ⟨h₁.conj_mem ⟨(n : G × N).fst, (mem_prod.mp n.2).1⟩ hgHK.1 ⟨(g : G × N).fst, (mem_prod.mp g.2).1⟩,
      h₂.conj_mem ⟨(n : G × N).snd, (mem_prod.mp n.2).2⟩ hgHK.2 ⟨(g : G × N).snd, (mem_prod.mp g.2).2⟩⟩

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