OAI/RepresentationTheory/PartialPermutation/DiagramCounts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PartialPermutation.DiagramCounting.rectangle_card_le line 11
  2. lemma OAI.PartialPermutation.DiagramCounting.cell_bounded line 20
  3. lemma OAI.PartialPermutation.DiagramCounting.rowLen_le_card line 25
  4. lemma OAI.PartialPermutation.DiagramCounting.colLen_le_card line 31
  5. def OAI.PartialPermutation.DiagramCounting.Shape line 37
  6. def OAI.PartialPermutation.DiagramCounting.boxCode line 39
  7. lemma OAI.PartialPermutation.DiagramCounting.boxCode_injective line 47
  8. instance OAI.PartialPermutation.DiagramCounting.(instance at line 53) line 53
  9. def OAI.PartialPermutation.DiagramCounting.partitionCount line 55
  10. def OAI.PartialPermutation.DiagramCounting.shortCode line 57
  11. lemma OAI.PartialPermutation.DiagramCounting.no_large_corner line 62
  12. lemma OAI.PartialPermutation.DiagramCounting.shortCode_injective line 71
  13. lemma OAI.PartialPermutation.DiagramCounting.partitionCount_le_shortCode line 102
  14. lemma OAI.PartialPermutation.DiagramCounting.partitionCount_le_sqrt line 108