noncenter — Mathlib

English

The nontrivial conjugacy classes of a group G are the conjugacy classes that are not the singleton {e}.

Русский

Нормальные коньюгейтные классы не тривиальны, то есть не являются единичными классами, состоящими только из тождественного элемента.

LaTeX

$$noncenter(G) = {x ∈ ConjClasses(G) : x.carrier.Nontrivial}$$

Lean4

/-- The conjugacy classes that are not trivial. -/
def noncenter (G : Type*) [Monoid G] : Set (ConjClasses G) :=
  {x | x.carrier.Nontrivial}

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