OAI/RepresentationTheory/UniversalSquare/Finite/DegreeEight.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

Degree Eight.

  1. def OAI.UniversalTensorSquare.eightWitness line 14
  2. lemma OAI.UniversalTensorSquare.eightWitness_cols line 16
  3. lemma OAI.UniversalTensorSquare.eightWitness_card line 19
  4. lemma OAI.UniversalTensorSquare.eightWitness_self line 22
  5. def OAI.UniversalTensorSquare.eightPlaceB0 line 26
  6. def OAI.UniversalTensorSquare.eightPlaceT0 line 28
  7. def OAI.UniversalTensorSquare.eightFlag0 line 30
  8. lemma OAI.UniversalTensorSquare.eightCertificate0 line 33
  9. def OAI.UniversalTensorSquare.eightPlaceB1 line 40
  10. def OAI.UniversalTensorSquare.eightPlaceT1 line 42
  11. def OAI.UniversalTensorSquare.eightFlag1 line 44
  12. lemma OAI.UniversalTensorSquare.eightCertificate1 line 47
  13. def OAI.UniversalTensorSquare.eightPlaceB2 line 54
  14. def OAI.UniversalTensorSquare.eightPlaceT2 line 56
  15. def OAI.UniversalTensorSquare.eightFlag2 line 58
  16. lemma OAI.UniversalTensorSquare.eightCertificate2 line 61
  17. def OAI.UniversalTensorSquare.eightPlaceB3 line 68
  18. def OAI.UniversalTensorSquare.eightPlaceT3 line 70
  19. def OAI.UniversalTensorSquare.eightFlag3 line 72
  20. lemma OAI.UniversalTensorSquare.eightCertificate3 line 75
  21. def OAI.UniversalTensorSquare.eightPlaceB4 line 82
  22. def OAI.UniversalTensorSquare.eightPlaceT4 line 84
  23. def OAI.UniversalTensorSquare.eightFlag4 line 86
  24. lemma OAI.UniversalTensorSquare.eightCertificate4 line 89
  25. def OAI.UniversalTensorSquare.eightPlaceB5 line 96
  26. def OAI.UniversalTensorSquare.eightPlaceT5 line 98
  27. def OAI.UniversalTensorSquare.eightFlag5 line 100
  28. lemma OAI.UniversalTensorSquare.eightCertificate5 line 103
  29. def OAI.UniversalTensorSquare.eightPlaceB6 line 110
  30. def OAI.UniversalTensorSquare.eightPlaceT6 line 112
  31. def OAI.UniversalTensorSquare.eightFlag6 line 114
  32. lemma OAI.UniversalTensorSquare.eightCertificate6 line 117
  33. def OAI.UniversalTensorSquare.eightPlaceB7 line 124
  34. def OAI.UniversalTensorSquare.eightPlaceT7 line 126
  35. def OAI.UniversalTensorSquare.eightFlag7 line 128
  36. lemma OAI.UniversalTensorSquare.eightCertificate7 line 131
  37. def OAI.UniversalTensorSquare.eightPlaceB8 line 138
  38. def OAI.UniversalTensorSquare.eightPlaceT8 line 140
  39. def OAI.UniversalTensorSquare.eightFlag8 line 142
  40. lemma OAI.UniversalTensorSquare.eightCertificate8 line 145
  41. def OAI.UniversalTensorSquare.eightPlaceB9 line 152
  42. def OAI.UniversalTensorSquare.eightPlaceT9 line 154
  43. def OAI.UniversalTensorSquare.eightFlag9 line 156
  44. lemma OAI.UniversalTensorSquare.eightCertificate9 line 159
  45. def OAI.UniversalTensorSquare.eightPlaceB11 line 166
  46. def OAI.UniversalTensorSquare.eightPlaceT11 line 168
  47. def OAI.UniversalTensorSquare.eightFlag11 line 170
  48. lemma OAI.UniversalTensorSquare.eightCertificate11 line 173
  49. lemma OAI.UniversalTensorSquare.eight_positive_certificate line 182
  50. lemma OAI.UniversalTensorSquare.eight_positive0 line 194
  51. lemma OAI.UniversalTensorSquare.eight_positive1 line 205
  52. lemma OAI.UniversalTensorSquare.eight_positive2 line 216
  53. lemma OAI.UniversalTensorSquare.eight_positive3 line 227
  54. lemma OAI.UniversalTensorSquare.eight_positive4 line 238
  55. lemma OAI.UniversalTensorSquare.eight_positive5 line 249
  56. lemma OAI.UniversalTensorSquare.eight_positive6 line 260
  57. lemma OAI.UniversalTensorSquare.eight_positive7 line 271
  58. lemma OAI.UniversalTensorSquare.eight_positive8 line 282
  59. lemma OAI.UniversalTensorSquare.eight_positive9 line 293
  60. lemma OAI.UniversalTensorSquare.eight_positive10 line 304
  61. lemma OAI.UniversalTensorSquare.eight_positive11 line 315
  62. lemma OAI.UniversalTensorSquare.eight_positive_target_eq line 326
  63. lemma OAI.UniversalTensorSquare.partitionLists_eight line 335
  64. theorem OAI.UniversalTensorSquare.eight_kronecker_pos line 338
  65. theorem OAI.UniversalTensorSquare.universal_tensor_square_eight line 464