commutator_eq_normalClosure — Mathlib

English

The commutator subgroup of G equals the normal closure of the set of all commutators in G.

Русский

Коммутаторная подгруппа G равна нормальному замыканию множества всех коммутаторов в G.

LaTeX

$$$ \\operatorname{commutator}(G) = \\operatorname{Subgroup.normalClosure}(\\operatorname{commutatorSet}(G)) $$$

Lean4

theorem commutator_eq_normalClosure : commutator G = Subgroup.normalClosure (commutatorSet G) := by
  simp [commutator, Subgroup.commutator_def', commutatorSet]

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