OAI/RepresentationTheory/PartialPermutation/Equivalences.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartialPermutation.subrepresentationCompEquiv line 22
  2. instance OAI.PartialPermutation.irreducible_comp_mulEquiv line 36
  3. def OAI.PartialPermutation.representationEquivComp line 41
  4. def OAI.PartialPermutation.representationEquivCompGeneral line 46
  5. def OAI.PartialPermutation.irreducibleIndexMap line 53
  6. lemma OAI.PartialPermutation.irreducibleIndexMap_spec line 56
  7. lemma OAI.PartialPermutation.irreducibleIndexMap_inverse line 61
  8. def OAI.PartialPermutation.irreducibleIndexEquiv line 83
  9. lemma OAI.PartialPermutation.irreducibleDegree_map line 89
  10. lemma OAI.PartialPermutation.inverseDegreeSum_equiv line 94