char_one

Mathlib.RepresentationTheory.Character

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

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_one (V : FDRep k G) : V.character 1 = Module.finrank k V := by simp only [character, map_one, trace_one]

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

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

Разделы

Аффилиация

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