OAI/RepresentationTheory/PartialPermutation/CompleteKernels.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartialPermutation.componentRepline 21 - instance
OAI.PartialPermutation.componentRep_irreducibleline 24 - lemma
OAI.PartialPermutation.componentRep_equiv_iffline 28 - lemma
OAI.PartialPermutation.complexFourier_subrepline 38 - lemma
OAI.PartialPermutation.complexFourier_sumline 45 - lemma
OAI.PartialPermutation.sum_character_kernels_identityline 50