character — Mathlib

English

For a finite-dimensional representation V : FDRep k G, the character is the function g ↦ trace(ρ_V(g)).

Русский

Для конечномерного представления V над k G характеристика — это функция, сопоставляющая каждому элементу g ∈ G след линейного преобразования ρ_V(g).

LaTeX

$$$\chi_V(g) = \operatorname{tr}_k\bigl( V.\rho(g) \bigr).$$$

Lean4

/-- The character of a representation `V : FDRep k G` is the function associating to `g : G` the
trace of the linear map `V.ρ g`. -/
def character (V : FDRep k G) (g : G) :=
  LinearMap.trace k V (V.ρ g)

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