char_mul_comm — Mathlib

English

For a representation V, the character is constant on conjugacy classes: χ(hgh^{-1}) = χ(g) for all g,h ∈ G.

Русский

Для представления характеристика константна по конъюгациям: χ(hgh^{-1}) = χ(g) для всех g,h ∈ G.

LaTeX

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

Lean4

theorem char_mul_comm (V : FDRep k G) (g : G) (h : G) : V.character (h * g) = V.character (g * h) := by
  simp only [trace_mul_comm, character, map_mul]

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