char_conj — Mathlib

English

The character is constant on conjugacy classes; equivalently, χ(hgh^{-1}) = χ(g).

Русский

Характер константен по конъюгациям; эквивалентно χ(hgh^{-1}) = χ(g).

LaTeX

$$$\chi_V(hgh^{-1}) = \chi_V(g).$$$

Lean4

/-- The character of a representation is constant on conjugacy classes. -/
@[simp]
theorem char_conj (V : FDRep k G) (g : G) (h : G) : V.character (h * g * h⁻¹) = V.character g := by
  rw [char_mul_comm, inv_mul_cancel_left]

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