Theorems · Definition · group theory
FDRep.character
{k : Type u} → [inst : Field k] → {G : Type v} → [inst_1 : Monoid G] → FDRep k G → G → kThe character of a representation V : FDRep k G is the function associating to g : G the
trace of the linear map V.ρ g.
- Defined in
- Mathlib.RepresentationTheory.Character
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- Monoidstatement and proof · cited by 3,887
- Action.Vproof · cited by 176
- LinearMap.traceproof · cited by 87
- FDRepstatement and proof · cited by 33
- FGModuleCat.carrierproof · cited by 28
- FDRep.ρproof · cited by 20
Cited by11
Results whose statement or proof uses this declaration.
- FDRep.scalar_product_char_eq_finrank_equivariantstatement and proof · cited by 2
- FDRep.average_char_eq_finrank_invariantsstatement and proof · cited by 1
- FDRep.char_dualstatement · cited by 1
- FDRep.char_isostatement · cited by 1
- FDRep.char_linHomstatement and proof · cited by 1
- FDRep.char_mul_commstatement · cited by 1
- FDRep.char_orthonormalstatement · cited by 1
- FDRep.char_tensorstatement and proof · cited by 1
- FDRep.char_conjstatement and proof · cited by 0
- FDRep.char_onestatement · cited by 0
- FDRep.simple_iff_char_is_norm_onestatement and proof · cited by 0