normal_subgroupOf_of_le_normalizer

English

If H ≤ N.normalizer, then N.subgroupOf H is normal.

Русский

Если H ≤ нормализатор N, то N.subgroupOf H нормальна.

LaTeX

$$H \le N.normalizer ⇒ (N.subgroupOf H).Normal$$

Lean4

@[to_additive]
theorem normal_subgroupOf_of_le_normalizer {H N : Subgroup G} (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal :=
  by
  rw [normal_subgroupOf_iff_le_normalizer_inf]
  exact (le_inf hLE H.le_normalizer).trans inf_normalizer_le_normalizer_inf

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