commutatorSet — Mathlib

English

The set commutatorSet(G) consists exactly of those elements g in G for which there exist g1,g2 ∈ G with [g1,g2] = g.

Русский

Множество commutatorSet(G) состоит ровно из тех элементов g ∈ G, для которых существуют g1,g2 ∈ G такие, что [g1,g2] = g.

LaTeX

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

Lean4

/-- The set of commutator elements `⁅g₁, g₂⁆` in `G`. -/
def commutatorSet : Set G :=
  {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}

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