OAI/RepresentationTheory/PartialPermutation/Model.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.IsUnitary line 9

   Also declared: ComparatorChallenges/PartialPermutation.lean:9 (same declaration text).

2. def OAI.PartialPermutation.hsNormSq line 16

   Also declared: ComparatorChallenges/PartialPermutation.lean:16 (same declaration text).

3. def OAI.PartialPermutation.complexFourier line 21

   Also declared: ComparatorChallenges/PartialPermutation.lean:21 (same declaration text).

4. def OAI.PartialPermutation.componentSimple line 27

   Also declared: ComparatorChallenges/PartialPermutation.lean:27 (same declaration text).

5. instance OAI.PartialPermutation.components_finite line 30

   Also declared: ComparatorChallenges/PartialPermutation.lean:30 (same declaration text).

6. def OAI.PartialPermutation.regularRep line 38

   Also declared: ComparatorChallenges/PartialPermutation.lean:38 (same declaration text).

7. abbrev OAI.PartialPermutation.IrreducibleIndex line 54

   Also declared: ComparatorChallenges/PartialPermutation.lean:54 (same declaration text).

8. instance OAI.PartialPermutation.irreducibleIndex_fintype line 57

   Also declared: ComparatorChallenges/PartialPermutation.lean:57 (same declaration text).

9. abbrev OAI.PartialPermutation.irreducibleSpace line 60

   Also declared: ComparatorChallenges/PartialPermutation.lean:60 (same declaration text).

10. abbrev OAI.PartialPermutation.irreducibleDegree line 63

    Also declared: ComparatorChallenges/PartialPermutation.lean:63 (same declaration text).

11. def OAI.PartialPermutation.mass line 67

    Also declared: ComparatorChallenges/PartialPermutation.lean:67 (same declaration text).

12. def OAI.PartialPermutation.LeftCosetCap line 69

    Also declared: ComparatorChallenges/PartialPermutation.lean:69 (same declaration text).

13. def OAI.PartialPermutation.blockSubgroup line 73

    Also declared: ComparatorChallenges/PartialPermutation.lean:73 (same declaration text).

14. def OAI.PartialPermutation.inverseDegreeSum line 84

    Also declared: ComparatorChallenges/PartialPermutation.lean:84 (same declaration text).

15. def OAI.PartialPermutation.symmetricInverseDegreeSum line 87

    Also declared: ComparatorChallenges/PartialPermutation.lean:87 (same declaration text).

16. def OAI.PartialPermutation.symmetricDegreeConstant line 90

    Also declared: ComparatorChallenges/PartialPermutation.lean:90 (same declaration text).

17. def OAI.PartialPermutation.ComplementaryCosetsFiniteStatement line 93

    Also declared: ComparatorChallenges/PartialPermutation.lean:93 (same declaration text).