OAI/RepresentationTheory/UniversalSquare/Support/CandidateRotation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Candidate Rotation.

  1. def OAI.UniversalTensorSquare.candidateBaseRotateCell line 15
  2. lemma OAI.UniversalTensorSquare.candidateBaseRotateCell_injective line 27
  3. def OAI.UniversalTensorSquare.candidateLastSwapCell line 39
  4. lemma OAI.UniversalTensorSquare.candidateLastSwapCell_injective line 49
  5. def OAI.UniversalTensorSquare.candidateRotateRow line 64
  6. lemma OAI.UniversalTensorSquare.candidateRotateRow_row line 71
  7. lemma OAI.UniversalTensorSquare.candidateRotateRow_mark line 74
  8. def OAI.UniversalTensorSquare.candidateSwap line 90
  9. def OAI.UniversalTensorSquare.candidateRotateCol line 104
  10. lemma OAI.UniversalTensorSquare.candidateRotateCol_col line 108
  11. lemma OAI.UniversalTensorSquare.candidateRotateCol_mark line 111
  12. def OAI.UniversalTensorSquare.candidateRotateRowPositions line 119
  13. def OAI.UniversalTensorSquare.candidateRotateColPositions line 127
  14. theorem OAI.UniversalTensorSquare.candidate_projected_ne_zero line 135