OAI/RepresentationTheory/UniversalSquare/Support/Candidate.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Candidate.

  1. def OAI.UniversalTensorSquare.rectangle line 14
  2. lemma OAI.UniversalTensorSquare.mem_rectangle line 21
  3. def OAI.UniversalTensorSquare.candidateArm line 26
  4. def OAI.UniversalTensorSquare.candidate line 29
  5. lemma OAI.UniversalTensorSquare.mem_candidate line 32
  6. lemma OAI.UniversalTensorSquare.candidate_transpose line 41
  7. def OAI.UniversalTensorSquare.armExtras line 48
  8. lemma OAI.UniversalTensorSquare.mem_armExtras line 52
  9. lemma OAI.UniversalTensorSquare.armExtras_card line 59
  10. lemma OAI.UniversalTensorSquare.staircase_disjoint_armExtras line 69
  11. lemma OAI.UniversalTensorSquare.armExtras_disjoint_transpose line 77
  12. lemma OAI.UniversalTensorSquare.candidate_cells line 87
  13. lemma OAI.UniversalTensorSquare.candidate_card line 98
  14. def OAI.UniversalTensorSquare.candidateLengths line 117
  15. lemma OAI.UniversalTensorSquare.candidate_rowLen line 124
  16. lemma OAI.UniversalTensorSquare.candidate_colLen line 138
  17. lemma OAI.UniversalTensorSquare.candidate_zero line 143
  18. def OAI.UniversalTensorSquare.fixedCandidate line 149
  19. lemma OAI.UniversalTensorSquare.fixedCandidate_transpose line 152
  20. lemma OAI.UniversalTensorSquare.fixedCandidate_eq_staircase_of_remainder_zero line 155
  21. lemma OAI.UniversalTensorSquare.fixedCandidate_card line 160
  22. theorem OAI.UniversalTensorSquare.fixedCandidate_large_degree line 166