OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLeaves4.lean

GitHub source file

200 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Leaves 4.

  1. def OAI.UniversalTensorSquare.sgB826 line 16
  2. def OAI.UniversalTensorSquare.sgT826 line 17
  3. def OAI.UniversalTensorSquare.sgFlag826 line 18
  4. lemma OAI.UniversalTensorSquare.sgCert826 line 19
  5. lemma OAI.UniversalTensorSquare.sg826 line 23
  6. def OAI.UniversalTensorSquare.sgB827 line 32
  7. def OAI.UniversalTensorSquare.sgT827 line 33
  8. def OAI.UniversalTensorSquare.sgFlag827 line 34
  9. lemma OAI.UniversalTensorSquare.sgCert827 line 35
  10. lemma OAI.UniversalTensorSquare.sg827 line 39
  11. def OAI.UniversalTensorSquare.sgB828 line 48
  12. def OAI.UniversalTensorSquare.sgT828 line 49
  13. def OAI.UniversalTensorSquare.sgFlag828 line 50
  14. lemma OAI.UniversalTensorSquare.sgCert828 line 51
  15. lemma OAI.UniversalTensorSquare.sg828 line 55
  16. def OAI.UniversalTensorSquare.sgB829 line 64
  17. def OAI.UniversalTensorSquare.sgT829 line 65
  18. def OAI.UniversalTensorSquare.sgFlag829 line 66
  19. lemma OAI.UniversalTensorSquare.sgCert829 line 67
  20. lemma OAI.UniversalTensorSquare.sg829 line 71
  21. def OAI.UniversalTensorSquare.sgB832 line 80
  22. def OAI.UniversalTensorSquare.sgT832 line 81
  23. def OAI.UniversalTensorSquare.sgFlag832 line 82
  24. lemma OAI.UniversalTensorSquare.sgCert832 line 83
  25. lemma OAI.UniversalTensorSquare.sg832 line 87
  26. def OAI.UniversalTensorSquare.sgB833 line 96
  27. def OAI.UniversalTensorSquare.sgT833 line 97
  28. def OAI.UniversalTensorSquare.sgFlag833 line 98
  29. lemma OAI.UniversalTensorSquare.sgCert833 line 99
  30. lemma OAI.UniversalTensorSquare.sg833 line 103
  31. def OAI.UniversalTensorSquare.sgB834 line 112
  32. def OAI.UniversalTensorSquare.sgT834 line 113
  33. def OAI.UniversalTensorSquare.sgFlag834 line 114
  34. lemma OAI.UniversalTensorSquare.sgCert834 line 115
  35. lemma OAI.UniversalTensorSquare.sg834 line 119
  36. def OAI.UniversalTensorSquare.sgB835 line 128
  37. def OAI.UniversalTensorSquare.sgT835 line 129
  38. def OAI.UniversalTensorSquare.sgFlag835 line 130
  39. lemma OAI.UniversalTensorSquare.sgCert835 line 131
  40. lemma OAI.UniversalTensorSquare.sg835 line 135
  41. def OAI.UniversalTensorSquare.sgB836 line 154
  42. def OAI.UniversalTensorSquare.sgT836 line 155
  43. def OAI.UniversalTensorSquare.sgFlag836 line 156
  44. lemma OAI.UniversalTensorSquare.sgCert836 line 157
  45. lemma OAI.UniversalTensorSquare.sg836 line 161
  46. def OAI.UniversalTensorSquare.sgB837 line 170
  47. def OAI.UniversalTensorSquare.sgT837 line 171
  48. def OAI.UniversalTensorSquare.sgFlag837 line 172
  49. lemma OAI.UniversalTensorSquare.sgCert837 line 173
  50. lemma OAI.UniversalTensorSquare.sg837 line 177
  51. def OAI.UniversalTensorSquare.sgB838 line 186
  52. def OAI.UniversalTensorSquare.sgT838 line 187
  53. def OAI.UniversalTensorSquare.sgFlag838 line 188
  54. lemma OAI.UniversalTensorSquare.sgCert838 line 189
  55. lemma OAI.UniversalTensorSquare.sg838 line 193
  56. def OAI.UniversalTensorSquare.sgB839 line 202
  57. def OAI.UniversalTensorSquare.sgT839 line 203
  58. def OAI.UniversalTensorSquare.sgFlag839 line 204
  59. lemma OAI.UniversalTensorSquare.sgCert839 line 205
  60. lemma OAI.UniversalTensorSquare.sg839 line 209
  61. def OAI.UniversalTensorSquare.sgB840 line 218
  62. def OAI.UniversalTensorSquare.sgT840 line 219
  63. def OAI.UniversalTensorSquare.sgFlag840 line 220
  64. lemma OAI.UniversalTensorSquare.sgCert840 line 221
  65. lemma OAI.UniversalTensorSquare.sg840 line 225
  66. def OAI.UniversalTensorSquare.sgB841 line 234
  67. def OAI.UniversalTensorSquare.sgT841 line 235
  68. def OAI.UniversalTensorSquare.sgFlag841 line 236
  69. lemma OAI.UniversalTensorSquare.sgCert841 line 237
  70. lemma OAI.UniversalTensorSquare.sg841 line 241
  71. def OAI.UniversalTensorSquare.sgB846 line 250
  72. def OAI.UniversalTensorSquare.sgT846 line 251
  73. def OAI.UniversalTensorSquare.sgFlag846 line 252
  74. lemma OAI.UniversalTensorSquare.sgCert846 line 253
  75. lemma OAI.UniversalTensorSquare.sg846 line 257
  76. def OAI.UniversalTensorSquare.sgB847 line 266
  77. def OAI.UniversalTensorSquare.sgT847 line 267
  78. def OAI.UniversalTensorSquare.sgFlag847 line 268
  79. lemma OAI.UniversalTensorSquare.sgCert847 line 269
  80. lemma OAI.UniversalTensorSquare.sg847 line 273
  81. def OAI.UniversalTensorSquare.sgB873 line 292
  82. def OAI.UniversalTensorSquare.sgT873 line 293
  83. def OAI.UniversalTensorSquare.sgFlag873 line 294
  84. lemma OAI.UniversalTensorSquare.sgCert873 line 295
  85. lemma OAI.UniversalTensorSquare.sg873 line 299
  86. def OAI.UniversalTensorSquare.sgB874 line 308
  87. def OAI.UniversalTensorSquare.sgT874 line 309
  88. def OAI.UniversalTensorSquare.sgFlag874 line 310
  89. lemma OAI.UniversalTensorSquare.sgCert874 line 311
  90. lemma OAI.UniversalTensorSquare.sg874 line 315
  91. def OAI.UniversalTensorSquare.sgB875 line 324
  92. def OAI.UniversalTensorSquare.sgT875 line 325
  93. def OAI.UniversalTensorSquare.sgFlag875 line 326
  94. lemma OAI.UniversalTensorSquare.sgCert875 line 327
  95. lemma OAI.UniversalTensorSquare.sg875 line 331
  96. def OAI.UniversalTensorSquare.sgB876 line 340
  97. def OAI.UniversalTensorSquare.sgT876 line 341
  98. def OAI.UniversalTensorSquare.sgFlag876 line 342
  99. lemma OAI.UniversalTensorSquare.sgCert876 line 343
  100. lemma OAI.UniversalTensorSquare.sg876 line 347
  101. def OAI.UniversalTensorSquare.sgB877 line 356
  102. def OAI.UniversalTensorSquare.sgT877 line 357
  103. def OAI.UniversalTensorSquare.sgFlag877 line 358
  104. lemma OAI.UniversalTensorSquare.sgCert877 line 359
  105. lemma OAI.UniversalTensorSquare.sg877 line 363
  106. def OAI.UniversalTensorSquare.sgB878 line 372
  107. def OAI.UniversalTensorSquare.sgT878 line 373
  108. def OAI.UniversalTensorSquare.sgFlag878 line 374
  109. lemma OAI.UniversalTensorSquare.sgCert878 line 375
  110. lemma OAI.UniversalTensorSquare.sg878 line 379
  111. def OAI.UniversalTensorSquare.sgB879 line 388
  112. def OAI.UniversalTensorSquare.sgT879 line 389
  113. def OAI.UniversalTensorSquare.sgFlag879 line 390
  114. lemma OAI.UniversalTensorSquare.sgCert879 line 391
  115. lemma OAI.UniversalTensorSquare.sg879 line 395
  116. def OAI.UniversalTensorSquare.sgB880 line 404
  117. def OAI.UniversalTensorSquare.sgT880 line 405
  118. def OAI.UniversalTensorSquare.sgFlag880 line 406
  119. lemma OAI.UniversalTensorSquare.sgCert880 line 407
  120. lemma OAI.UniversalTensorSquare.sg880 line 411
  121. def OAI.UniversalTensorSquare.sgB881 line 430
  122. def OAI.UniversalTensorSquare.sgT881 line 431
  123. def OAI.UniversalTensorSquare.sgFlag881 line 432
  124. lemma OAI.UniversalTensorSquare.sgCert881 line 433
  125. lemma OAI.UniversalTensorSquare.sg881 line 437
  126. def OAI.UniversalTensorSquare.sgB884 line 446
  127. def OAI.UniversalTensorSquare.sgT884 line 447
  128. def OAI.UniversalTensorSquare.sgFlag884 line 448
  129. lemma OAI.UniversalTensorSquare.sgCert884 line 449
  130. lemma OAI.UniversalTensorSquare.sg884 line 453
  131. def OAI.UniversalTensorSquare.sgB885 line 462
  132. def OAI.UniversalTensorSquare.sgT885 line 463
  133. def OAI.UniversalTensorSquare.sgFlag885 line 464
  134. lemma OAI.UniversalTensorSquare.sgCert885 line 465
  135. lemma OAI.UniversalTensorSquare.sg885 line 469
  136. def OAI.UniversalTensorSquare.sgB886 line 478
  137. def OAI.UniversalTensorSquare.sgT886 line 479
  138. def OAI.UniversalTensorSquare.sgFlag886 line 480
  139. lemma OAI.UniversalTensorSquare.sgCert886 line 481
  140. lemma OAI.UniversalTensorSquare.sg886 line 485
  141. def OAI.UniversalTensorSquare.sgB887 line 494
  142. def OAI.UniversalTensorSquare.sgT887 line 495
  143. def OAI.UniversalTensorSquare.sgFlag887 line 496
  144. lemma OAI.UniversalTensorSquare.sgCert887 line 497
  145. lemma OAI.UniversalTensorSquare.sg887 line 501
  146. def OAI.UniversalTensorSquare.sgB889 line 510
  147. def OAI.UniversalTensorSquare.sgT889 line 511
  148. def OAI.UniversalTensorSquare.sgFlag889 line 512
  149. lemma OAI.UniversalTensorSquare.sgCert889 line 513
  150. lemma OAI.UniversalTensorSquare.sg889 line 517
  151. def OAI.UniversalTensorSquare.sgB890 line 526
  152. def OAI.UniversalTensorSquare.sgT890 line 527
  153. def OAI.UniversalTensorSquare.sgFlag890 line 528
  154. lemma OAI.UniversalTensorSquare.sgCert890 line 529
  155. lemma OAI.UniversalTensorSquare.sg890 line 533
  156. def OAI.UniversalTensorSquare.sgB891 line 542
  157. def OAI.UniversalTensorSquare.sgT891 line 543
  158. def OAI.UniversalTensorSquare.sgFlag891 line 544
  159. lemma OAI.UniversalTensorSquare.sgCert891 line 545
  160. lemma OAI.UniversalTensorSquare.sg891 line 549
  161. def OAI.UniversalTensorSquare.sgB892 line 568
  162. def OAI.UniversalTensorSquare.sgT892 line 569
  163. def OAI.UniversalTensorSquare.sgFlag892 line 570
  164. lemma OAI.UniversalTensorSquare.sgCert892 line 571
  165. lemma OAI.UniversalTensorSquare.sg892 line 575
  166. def OAI.UniversalTensorSquare.sgB897 line 584
  167. def OAI.UniversalTensorSquare.sgT897 line 585
  168. def OAI.UniversalTensorSquare.sgFlag897 line 586
  169. lemma OAI.UniversalTensorSquare.sgCert897 line 587
  170. lemma OAI.UniversalTensorSquare.sg897 line 591
  171. def OAI.UniversalTensorSquare.sgB898 line 600
  172. def OAI.UniversalTensorSquare.sgT898 line 601
  173. def OAI.UniversalTensorSquare.sgFlag898 line 602
  174. lemma OAI.UniversalTensorSquare.sgCert898 line 603
  175. lemma OAI.UniversalTensorSquare.sg898 line 607
  176. def OAI.UniversalTensorSquare.sgB899 line 616
  177. def OAI.UniversalTensorSquare.sgT899 line 617
  178. def OAI.UniversalTensorSquare.sgFlag899 line 618
  179. lemma OAI.UniversalTensorSquare.sgCert899 line 619
  180. lemma OAI.UniversalTensorSquare.sg899 line 623
  181. def OAI.UniversalTensorSquare.sgB902 line 632
  182. def OAI.UniversalTensorSquare.sgT902 line 633
  183. def OAI.UniversalTensorSquare.sgFlag902 line 634
  184. lemma OAI.UniversalTensorSquare.sgCert902 line 635
  185. lemma OAI.UniversalTensorSquare.sg902 line 639
  186. def OAI.UniversalTensorSquare.sgB903 line 648
  187. def OAI.UniversalTensorSquare.sgT903 line 649
  188. def OAI.UniversalTensorSquare.sgFlag903 line 650
  189. lemma OAI.UniversalTensorSquare.sgCert903 line 651
  190. lemma OAI.UniversalTensorSquare.sg903 line 655
  191. def OAI.UniversalTensorSquare.sgB909 line 664
  192. def OAI.UniversalTensorSquare.sgT909 line 665
  193. def OAI.UniversalTensorSquare.sgFlag909 line 666
  194. lemma OAI.UniversalTensorSquare.sgCert909 line 667
  195. lemma OAI.UniversalTensorSquare.sg909 line 671
  196. def OAI.UniversalTensorSquare.sgB915 line 680
  197. def OAI.UniversalTensorSquare.sgT915 line 681
  198. def OAI.UniversalTensorSquare.sgFlag915 line 682
  199. lemma OAI.UniversalTensorSquare.sgCert915 line 683
  200. lemma OAI.UniversalTensorSquare.sg915 line 687