char_tensor — Mathlib

English

The character is multiplicative under tensor product: χ_{V⊗W} = χ_V · χ_W.

Русский

Характер тензорного произведения линейно суммируется: χ_{V⊗W} = χ_V · χ_W.

LaTeX

$$$\chi_{V \otimes W} = \chi_V \cdot \chi_W.$$$

Lean4

/-- The character is multiplicative under the tensor product. -/
@[simp]
theorem char_tensor (V W : FDRep k G) : (V ⊗ W).character = V.character * W.character := by ext g;
  convert trace_tensorProduct' (V.ρ g) (W.ρ g)

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