normal_inf_normal — Mathlib

English

The intersection of two normal subgroups is normal.

Русский

Пересечение двух нормальных подгрупп относится к нормальным.

LaTeX

$$$(H \triangleleft G) \land (K \triangleleft G) \Rightarrow (H \cap K) \trianglelefteq G$$$

Lean4

@[to_additive]
instance normal_inf_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal :=
  ⟨fun n hmem g => ⟨hH.conj_mem n hmem.1 g, hK.conj_mem n hmem.2 g⟩⟩

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