OAI/RepresentationTheory/UniversalSquare/Support/CandidateSupport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Candidate Support.

  1. theorem OAI.Saxl.kronecker_pos_of_tensor_cyclic_support line 16
  2. lemma OAI.Saxl.pairWord_mem_alphabetLeft_gen line 49
  3. theorem OAI.UniversalTensorSquare.kronecker_pos_of_rowColumn_support line 62
  4. lemma OAI.UniversalTensorSquare.candidateHighLetter_injective line 86
  5. lemma OAI.UniversalTensorSquare.candidateHighMap_injective line 97
  6. lemma OAI.UniversalTensorSquare.candidateHighLetter_marked line 104
  7. lemma OAI.UniversalTensorSquare.candidateHighWord_alphabet line 112
  8. lemma OAI.UniversalTensorSquare.candidateBandRow_alphabet line 122
  9. lemma OAI.UniversalTensorSquare.candidateBandWord_alphabet line 135
  10. lemma OAI.UniversalTensorSquare.candidateBandWord_ne_zero line 142
  11. theorem OAI.UniversalTensorSquare.candidateHighWord_support line 151
  12. theorem OAI.UniversalTensorSquare.candidate_triangle_quotient line 159
  13. theorem OAI.UniversalTensorSquare.candidate_cut_strip_support line 169
  14. theorem OAI.UniversalTensorSquare.candidate_kronecker_pos_of_strip_band line 189