OAI/RepresentationTheory/UniversalSquare/Finite/DegreeFive.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Degree Five.

  1. def OAI.UniversalTensorSquare.fiveWitness line 15
  2. lemma OAI.UniversalTensorSquare.fiveWitness_cols line 17
  3. lemma OAI.UniversalTensorSquare.fiveWitness_card line 20
  4. lemma OAI.UniversalTensorSquare.fiveWitness_self line 23
  5. def OAI.UniversalTensorSquare.hookPlacement line 27
  6. def OAI.UniversalTensorSquare.flag5 line 29
  7. def OAI.UniversalTensorSquare.flag41 line 33
  8. def OAI.UniversalTensorSquare.flag32 line 37
  9. def OAI.UniversalTensorSquare.flag311 line 41
  10. lemma OAI.UniversalTensorSquare.certificate5 line 45
  11. lemma OAI.UniversalTensorSquare.certificate41 line 48
  12. lemma OAI.UniversalTensorSquare.certificate32 line 51
  13. lemma OAI.UniversalTensorSquare.certificate311 line 54
  14. lemma OAI.UniversalTensorSquare.five_positive_certificate line 60
  15. lemma OAI.UniversalTensorSquare.five_positive5 line 72
  16. lemma OAI.UniversalTensorSquare.five_positive41 line 83
  17. lemma OAI.UniversalTensorSquare.five_positive32 line 94
  18. lemma OAI.UniversalTensorSquare.five_positive311 line 105
  19. lemma OAI.UniversalTensorSquare.five_positive_target_eq line 115
  20. lemma OAI.UniversalTensorSquare.partitionLists_five line 124
  21. theorem OAI.UniversalTensorSquare.five_kronecker_pos line 127
  22. theorem OAI.UniversalTensorSquare.universal_tensor_square_five line 173