char_linHom — Mathlib

English

The character of the linear maps between V and W equals χ_V(g^{-1}) · χ_W(g).

Русский

Характер отображения линейных отображений между V и W равен χ_V(g^{-1}) · χ_W(g).

LaTeX

$$$\chi_{\mathrm{linHom}(V,W)}(g) = \chi_V(g^{-1}) \cdot \chi_W(g).$$$

Lean4

@[simp]
theorem char_linHom (V W : FDRep k G) (g : G) : (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g :=
  by rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]

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