OAI/RepresentationTheory/PartialPermutation/SmallKernels.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.smallTypeKernel line 18
2. lemma OAI.PartialPermutation.smallTypeKernel_inv line 22
3. lemma OAI.PartialPermutation.complexFourier_smallTypeKernel line 29
4. lemma OAI.PartialPermutation.hsNormSq_one line 61
5. lemma OAI.PartialPermutation.degree_le_of_kernel_identity line 65
6. lemma OAI.PartialPermutation.smallTypeKernel_identity_of_kernel line 77