OAI/RepresentationTheory/UniversalSquare/Finite/DegreeSeven.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Degree Seven.

  1. def OAI.UniversalTensorSquare.sevenWitness line 15
  2. lemma OAI.UniversalTensorSquare.sevenWitness_cols line 17
  3. lemma OAI.UniversalTensorSquare.sevenWitness_card line 20
  4. lemma OAI.UniversalTensorSquare.sevenWitness_self line 23
  5. def OAI.UniversalTensorSquare.sevenPlaceB0 line 27
  6. def OAI.UniversalTensorSquare.sevenPlaceT0 line 29
  7. def OAI.UniversalTensorSquare.sevenFlag0 line 31
  8. lemma OAI.UniversalTensorSquare.sevenCertificate0 line 34
  9. def OAI.UniversalTensorSquare.sevenPlaceB1 line 41
  10. def OAI.UniversalTensorSquare.sevenPlaceT1 line 43
  11. def OAI.UniversalTensorSquare.sevenFlag1 line 45
  12. lemma OAI.UniversalTensorSquare.sevenCertificate1 line 48
  13. def OAI.UniversalTensorSquare.sevenPlaceB2 line 55
  14. def OAI.UniversalTensorSquare.sevenPlaceT2 line 57
  15. def OAI.UniversalTensorSquare.sevenFlag2 line 59
  16. lemma OAI.UniversalTensorSquare.sevenCertificate2 line 62
  17. def OAI.UniversalTensorSquare.sevenPlaceB3 line 69
  18. def OAI.UniversalTensorSquare.sevenPlaceT3 line 71
  19. def OAI.UniversalTensorSquare.sevenFlag3 line 73
  20. lemma OAI.UniversalTensorSquare.sevenCertificate3 line 76
  21. def OAI.UniversalTensorSquare.sevenPlaceB4 line 83
  22. def OAI.UniversalTensorSquare.sevenPlaceT4 line 85
  23. def OAI.UniversalTensorSquare.sevenFlag4 line 87
  24. lemma OAI.UniversalTensorSquare.sevenCertificate4 line 90
  25. def OAI.UniversalTensorSquare.sevenPlaceB5 line 97
  26. def OAI.UniversalTensorSquare.sevenPlaceT5 line 99
  27. def OAI.UniversalTensorSquare.sevenFlag5 line 101
  28. lemma OAI.UniversalTensorSquare.sevenCertificate5 line 104
  29. def OAI.UniversalTensorSquare.sevenPlaceB6 line 111
  30. def OAI.UniversalTensorSquare.sevenPlaceT6 line 113
  31. def OAI.UniversalTensorSquare.sevenFlag6 line 115
  32. lemma OAI.UniversalTensorSquare.sevenCertificate6 line 118
  33. def OAI.UniversalTensorSquare.sevenPlaceB7 line 125
  34. def OAI.UniversalTensorSquare.sevenPlaceT7 line 127
  35. def OAI.UniversalTensorSquare.sevenFlag7 line 129
  36. lemma OAI.UniversalTensorSquare.sevenCertificate7 line 132
  37. lemma OAI.UniversalTensorSquare.seven_positive_certificate line 141
  38. lemma OAI.UniversalTensorSquare.seven_positive0 line 153
  39. lemma OAI.UniversalTensorSquare.seven_positive1 line 164
  40. lemma OAI.UniversalTensorSquare.seven_positive2 line 175
  41. lemma OAI.UniversalTensorSquare.seven_positive3 line 186
  42. lemma OAI.UniversalTensorSquare.seven_positive4 line 197
  43. lemma OAI.UniversalTensorSquare.seven_positive5 line 208
  44. lemma OAI.UniversalTensorSquare.seven_positive6 line 219
  45. lemma OAI.UniversalTensorSquare.seven_positive7 line 230
  46. lemma OAI.UniversalTensorSquare.seven_positive_target_eq line 241
  47. lemma OAI.UniversalTensorSquare.partitionLists_seven line 250
  48. theorem OAI.UniversalTensorSquare.seven_kronecker_pos line 253
  49. theorem OAI.UniversalTensorSquare.universal_tensor_square_seven line 343