commutatorSet_def — Mathlib

English

The set commutatorSet(G) is the collection of all elements that can be written as [g1,g2] with g1,g2 ∈ G.

Русский

Множество commutatorSet(G) состоит из всех элементов, которые можно записать в виде [g1,g2] при g1,g2 ∈ G.

LaTeX

$$$ commutatorSet(G) = \\{ g \\in G \\mid \\exists g_1,g_2 \\in G, [g_1,g_2] = g \\}$$$

Lean4

theorem commutatorSet_def : commutatorSet G = {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} :=
  rfl

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