OAI/RepresentationTheory/PartialPermutation/TrivialRepresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartialPermutation.trivialSubmoduleEquiv line 18
  2. instance OAI.PartialPermutation.trivial_rep_irreducible line 25
  3. lemma OAI.PartialPermutation.trivial_character line 29
  4. def OAI.PartialPermutation.trivialIndex line 32
  5. lemma OAI.PartialPermutation.trivialIndex_equiv line 35
  6. lemma OAI.PartialPermutation.trivialIndex_unique line 40
  7. lemma OAI.PartialPermutation.irreducibleDegree_trivial line 50
  8. lemma OAI.PartialPermutation.irreducibleRep_trivial_apply line 54
  9. lemma OAI.PartialPermutation.complexFourier_trivial line 62
  10. lemma OAI.PartialPermutation.complexFourier_uniform line 66
  11. lemma OAI.PartialPermutation.complexFourier_centered line 76