char_iso — Mathlib

English

Isomorphic representations have identical characters: if V ≅ W, then χ_V = χ_W.

Русский

Изоморфные представления имеют одинаковые характеристики: если V ≅ W, то χ_V = χ_W.

LaTeX

$$$\text{If } V \cong W, \text{ then } \chi_V = \chi_W.$$$

Lean4

/-- The character of isomorphic representations is the same. -/
theorem char_iso {V W : FDRep k G} (i : V ≅ W) : V.character = W.character :=
  by
  ext g
  simp only [character, FDRep.Iso.conj_ρ i]
  exact (trace_conj' (V.ρ g) _).symm

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