inf_subgroupOf_inf_normal_of_right

English

Let A, B, B' be subgroups of G with B' ≤ B and B' normal in B. Then (A ∩ B') is normal in (A ∩ B).

Русский

Пусть A, B, B' — подгруппы G с B' ≤ B и B' нормальна в B. Тогда A ∩ B' нормальна в A ∩ B.

LaTeX

$$((A ∩ B').Normal) in (A ∩ B)$$

Lean4

@[to_additive]
theorem inf_subgroupOf_inf_normal_of_right (A B' B : Subgroup G) [hN : (B'.subgroupOf B).Normal] :
    ((A ⊓ B').subgroupOf (A ⊓ B)).Normal :=
  by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf A.le_normalizer hN) (inf_normalizer_le_normalizer_inf)

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