OAI/RepresentationTheory/PartialPermutation/IsotypicMatrices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PartialPermutation.simple_action_surjective line 22
  2. def OAI.PartialPermutation.diagonalEnd line 41
  3. def OAI.PartialPermutation.isotypicLift line 55
  4. lemma OAI.PartialPermutation.isotypicLift_action line 59
  5. lemma OAI.PartialPermutation.isotypicLift_range line 67
  6. def OAI.PartialPermutation.isotypicOrbitMap line 73
  7. lemma OAI.PartialPermutation.mem_isotypicOrbitMap_range line 79
  8. lemma OAI.PartialPermutation.isotypicOrbitMap_range_invariant line 84
  9. lemma OAI.PartialPermutation.finrank_isotypicOrbitMap_range line 93
  10. structure OAI.PartialPermutation.IsotypicMatrixModel line 103
  11. lemma OAI.PartialPermutation.exists_isotypicMatrixModel line 112