Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 13:45 119e166b

View on Github →

feat(representation_theory/character): formula for the dimension of the invariants in terms of the character (#15084)

Estimated changes

Modified src/representation_theory/character.lean

added theorem fdRep.average_char_eq_finrank_invariants

Modified src/representation_theory/invariants.lean

deleted theorem group_algebra.average_def