mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(representation_theory/character): orthogonality of characters

Open antoinelab01 opened this issue 3 years ago • 1 comments

Orthogonality of characters for representations of finite groups

  • [ ] depends on: #13789
  • [ ] depends on: #13794

Open in Gitpod

antoinelab01 avatar Aug 13 '22 19:08 antoinelab01

This PR/issue depends on:

  • leanprover-community/mathlib#13789
  • leanprover-community/mathlib#13794 By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Aug 13 '22 19:08 mathlib-dependent-issues-bot

This PR/issue depends on:

  • ~~leanprover-community/mathlib#13789~~
  • ~~leanprover-community/mathlib#13794~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Nov 03 '22 14:11 mathlib-dependent-issues-bot

Very nice! I feel like this is a bit of a highlight --- what would you think about writing the human readable proof as comments interspersed in the proof here?

kim-em avatar Nov 04 '22 13:11 kim-em

bors merge

kim-em avatar Nov 09 '22 02:11 kim-em

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Nov 09 '22 06:11 bors[bot]