Theorems · Theorem · group theory

Representation.norm_ofDistribMulAction_eq

∀ {k : Type u_1} {A : Type u_3} [inst : Semiring k] [inst_1 : AddCommMonoid A] [inst_2 : Module k A] {G : Type u_4}
  [inst_3 : Group G] [inst_4 : Fintype G] [inst_5 : DistribMulAction G A] [inst_6 : SMulCommClass G k A] (x : A),
  (Representation.ofDistribMulAction k G A).norm x = ∑ g, g • x

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModuleGroupFintypeDistribMulActionSMulCommClass