OAI/RepresentationTheory/UniversalSquare/Support/CandidateCut.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Candidate Cut.

  1. def OAI.UniversalTensorSquare.candidateCutRow line 17
  2. def OAI.UniversalTensorSquare.candidateCutCol line 21
  3. lemma OAI.UniversalTensorSquare.candidateRotatePositions_sign line 25
  4. theorem OAI.UniversalTensorSquare.candidate_cut_layers line 40
  5. def OAI.UniversalTensorSquare.candidateHighPositions line 66
  6. abbrev OAI.UniversalTensorSquare.candidateBandSize line 77
  7. def OAI.UniversalTensorSquare.candidateCutPositions line 80
  8. lemma OAI.UniversalTensorSquare.candidateCutPositions_high line 88
  9. lemma OAI.UniversalTensorSquare.candidateCutPositions_left line 94
  10. lemma OAI.UniversalTensorSquare.candidateBandSize_add line 100
  11. def OAI.UniversalTensorSquare.candidateHighLetter line 105
  12. def OAI.UniversalTensorSquare.candidateHighRowLetter line 114
  13. lemma OAI.UniversalTensorSquare.candidateRotateRow_triangle line 119
  14. lemma OAI.UniversalTensorSquare.candidateRotateCol_triangle line 131
  15. lemma OAI.UniversalTensorSquare.candidate_highRow_word line 139
  16. lemma OAI.UniversalTensorSquare.candidate_highCol_word line 155
  17. def OAI.UniversalTensorSquare.candidateBandTableau line 170
  18. def OAI.UniversalTensorSquare.candidateBandRow line 174
  19. def OAI.UniversalTensorSquare.candidateBandCol line 179
  20. lemma OAI.UniversalTensorSquare.candidate_row_cut_group line 184
  21. lemma OAI.UniversalTensorSquare.candidate_col_cut_group line 193
  22. theorem OAI.UniversalTensorSquare.candidateCutRow_factor line 202
  23. theorem OAI.UniversalTensorSquare.candidateCutCol_factor line 217
  24. def OAI.UniversalTensorSquare.candidateHighMap line 232
  25. def OAI.UniversalTensorSquare.candidateHighWord line 236
  26. def OAI.UniversalTensorSquare.candidateBandWord line 239
  27. theorem OAI.UniversalTensorSquare.candidate_cut_factor line 242