char_dual

Mathlib.RepresentationTheory.Character

URI: https://scilib.ai/kg/mathlib#FDRep.char_dual

English

The character of the dual representation satisfies χ_{V^*}(g) = χ_V(g^{-1}).

Русский

Характер двойственного представления: χ_{V^*}(g) = χ_V(g^{-1}).

LaTeX

$$$\chi_{V^*}(g) = \chi_V(g^{-1}).$$$

Lean4

@[simp]
theorem char_dual (V : FDRep k G) (g : G) : (of (dual V.ρ)).character g = V.character g⁻¹ :=
  trace_transpose' (V.ρ g⁻¹)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru