normalClosure_normal — Mathlib

English

The normal closure of a set is a normal subgroup of the ambient group.

Русский

Нормальное замыкание множества является нормальной подгруппой окружающей группы.

LaTeX

$$$ \operatorname{normalClosure}(s) \trianglelefteq G $$$

Lean4

/-- The normal closure of `s` is a normal subgroup. -/
instance normalClosure_normal : (normalClosure s).Normal :=
  ⟨fun n h g =>
    by
    refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) h
    · exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
    · simp
    · rw [← conj_mul]
      exact mul_mem ihx ihy
    · rw [← conj_inv]
      exact inv_mem ihx⟩

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