normalClosure — Mathlib

English

The normal closure of a set s is defined as the subgroup closure of all conjugates of elements of s; it is the smallest normal subgroup containing s.

Русский

Нормальное замыкание множества s определяется как порожденная им подгруппа, порожденная всеми конъюгатами элементов s; это наименьшая нормальная подгруппа, содержащая s.

LaTeX

$$$ \operatorname{normalClosure}(s) = \mathrm{closure}(\mathrm{conjugatesOfSet}(s)) $$$

Lean4

/-- The normal closure of a set `s` is the subgroup closure of all the conjugates of
elements of `s`. It is the smallest normal subgroup containing `s`. -/
def normalClosure (s : Set G) : Subgroup G :=
  closure (conjugatesOfSet s)

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