commutator_eq_closure — Mathlib

English

The commutator subgroup of G equals the closure of the set of commutator elements in G.

Русский

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

LaTeX

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

Lean4

theorem commutator_eq_closure : commutator G = Subgroup.closure (commutatorSet G) := by
  simp [commutator, Subgroup.commutator_def, commutatorSet]

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