OAI/RepresentationTheory/UniversalSquare/Band/BandFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Band Factor.

  1. def OAI.UniversalTensorSquare.candidatePathRow line 17
  2. def OAI.UniversalTensorSquare.candidatePathCol line 23
  3. def OAI.UniversalTensorSquare.bandLongRowLetter line 29
  4. def OAI.UniversalTensorSquare.bandShortRowLetter line 33
  5. def OAI.UniversalTensorSquare.bandLongColLetter line 37
  6. def OAI.UniversalTensorSquare.bandShortColLetter line 41
  7. lemma OAI.UniversalTensorSquare.candidateBandRow_extras line 45
  8. lemma OAI.UniversalTensorSquare.candidateBandCol_extras line 59
  9. lemma OAI.UniversalTensorSquare.candidateBandRow_factor line 73
  10. lemma OAI.UniversalTensorSquare.candidateBandCol_factor line 86