fixedPoints_eq_center — Mathlib

English

The fixed points of the conjugation action on G are precisely the center of G.

Русский

Фиксированные точки действия сопряжения на G образуют центр G.

LaTeX

$$$\operatorname{fixedPoints}(\operatorname{ConjAct} G)\,G = \operatorname{center} G$$$

Lean4

/-- The set of fixed points of the conjugation action of `G` on itself is the center of `G`. -/
theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G :=
  by
  ext x
  simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

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