OAI/RepresentationTheory/UniversalSquare/Support/CandidateClearance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Candidate Clearance.

  1. lemma OAI.Saxl.altWord_support line 15
  2. lemma OAI.UniversalTensorSquare.candidateRotateRow_small line 32
  3. lemma OAI.UniversalTensorSquare.candidateRotateCol_small line 47
  4. lemma OAI.UniversalTensorSquare.candidateBandTableau_outside line 55
  5. lemma OAI.UniversalTensorSquare.candidateBandRow_seed line 66
  6. lemma OAI.UniversalTensorSquare.candidateBandCol_seed line 75
  7. theorem OAI.UniversalTensorSquare.candidateBandRow_clearance line 84
  8. theorem OAI.UniversalTensorSquare.candidateBandCol_clearance line 96
  9. def OAI.UniversalTensorSquare.candidatePathAlphabet line 108
  10. theorem OAI.UniversalTensorSquare.candidateBandWord_clearance line 112
  11. theorem OAI.UniversalTensorSquare.candidateBandWord_path_clearance line 124