normal_subgroupOf_iff_le_normalizer_inf

English

For H, K subgroups of G, (H.subgroupOf K).Normal is equivalent to K ≤ (H ⊓ K).normalizer.

Русский

Для подгрупп H, K: (H.subgroupOf K).Normal эквивалентно K ≤ (H ⊓ K).normalizer.

LaTeX

$$$(H.\mathrm{subgroupOf} K).Normal \iff K \le (H \cap K).\mathrm{normalizer}$$$

Lean4

@[to_additive]
theorem normal_subgroupOf_iff_le_normalizer_inf : (H.subgroupOf K).Normal ↔ K ≤ (H ⊓ K).normalizer :=
  inf_subgroupOf_right H K ▸ normal_subgroupOf_iff_le_normalizer inf_le_right

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