Theorems · Theorem · group theory

FDRep.scalar_product_char_eq_finrank_equivariant

∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] [Invertible ↑(Nat.card G)]
  (V W : FDRep k G), (↑(Nat.card G))⁻¹ * ∑ g, W.character g * V.character g⁻¹ = ↑(Module.finrank k (V ⟶ W))

If V and W are finite-dimensional representations of a finite group, then the scalar product of their characters is equal to the dimension of the space of equivariant maps from V to W.

Defined in

Mathlib.RepresentationTheory.Character

Cited by

2 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldGroupFintypeInvertible