OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLeaves1.lean

GitHub source file

200 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Leaves 1.

  1. def OAI.UniversalTensorSquare.sgB10 line 16
  2. def OAI.UniversalTensorSquare.sgT10 line 17
  3. def OAI.UniversalTensorSquare.sgFlag10 line 18
  4. lemma OAI.UniversalTensorSquare.sgCert10 line 19
  5. lemma OAI.UniversalTensorSquare.sg10 line 23
  6. def OAI.UniversalTensorSquare.sgB17 line 32
  7. def OAI.UniversalTensorSquare.sgT17 line 33
  8. def OAI.UniversalTensorSquare.sgFlag17 line 34
  9. lemma OAI.UniversalTensorSquare.sgCert17 line 35
  10. lemma OAI.UniversalTensorSquare.sg17 line 39
  11. def OAI.UniversalTensorSquare.sgB67 line 48
  12. def OAI.UniversalTensorSquare.sgT67 line 49
  13. def OAI.UniversalTensorSquare.sgFlag67 line 50
  14. lemma OAI.UniversalTensorSquare.sgCert67 line 51
  15. lemma OAI.UniversalTensorSquare.sg67 line 55
  16. def OAI.UniversalTensorSquare.sgB68 line 64
  17. def OAI.UniversalTensorSquare.sgT68 line 65
  18. def OAI.UniversalTensorSquare.sgFlag68 line 66
  19. lemma OAI.UniversalTensorSquare.sgCert68 line 67
  20. lemma OAI.UniversalTensorSquare.sg68 line 71
  21. def OAI.UniversalTensorSquare.sgB71 line 80
  22. def OAI.UniversalTensorSquare.sgT71 line 81
  23. def OAI.UniversalTensorSquare.sgFlag71 line 82
  24. lemma OAI.UniversalTensorSquare.sgCert71 line 83
  25. lemma OAI.UniversalTensorSquare.sg71 line 87
  26. def OAI.UniversalTensorSquare.sgB88 line 96
  27. def OAI.UniversalTensorSquare.sgT88 line 97
  28. def OAI.UniversalTensorSquare.sgFlag88 line 98
  29. lemma OAI.UniversalTensorSquare.sgCert88 line 99
  30. lemma OAI.UniversalTensorSquare.sg88 line 103
  31. def OAI.UniversalTensorSquare.sgB89 line 112
  32. def OAI.UniversalTensorSquare.sgT89 line 113
  33. def OAI.UniversalTensorSquare.sgFlag89 line 114
  34. lemma OAI.UniversalTensorSquare.sgCert89 line 115
  35. lemma OAI.UniversalTensorSquare.sg89 line 119
  36. def OAI.UniversalTensorSquare.sgB92 line 128
  37. def OAI.UniversalTensorSquare.sgT92 line 129
  38. def OAI.UniversalTensorSquare.sgFlag92 line 130
  39. lemma OAI.UniversalTensorSquare.sgCert92 line 131
  40. lemma OAI.UniversalTensorSquare.sg92 line 135
  41. def OAI.UniversalTensorSquare.sgB143 line 154
  42. def OAI.UniversalTensorSquare.sgT143 line 155
  43. def OAI.UniversalTensorSquare.sgFlag143 line 156
  44. lemma OAI.UniversalTensorSquare.sgCert143 line 157
  45. lemma OAI.UniversalTensorSquare.sg143 line 161
  46. def OAI.UniversalTensorSquare.sgB144 line 170
  47. def OAI.UniversalTensorSquare.sgT144 line 171
  48. def OAI.UniversalTensorSquare.sgFlag144 line 172
  49. lemma OAI.UniversalTensorSquare.sgCert144 line 173
  50. lemma OAI.UniversalTensorSquare.sg144 line 177
  51. def OAI.UniversalTensorSquare.sgB154 line 186
  52. def OAI.UniversalTensorSquare.sgT154 line 187
  53. def OAI.UniversalTensorSquare.sgFlag154 line 188
  54. lemma OAI.UniversalTensorSquare.sgCert154 line 189
  55. lemma OAI.UniversalTensorSquare.sg154 line 193
  56. def OAI.UniversalTensorSquare.sgB155 line 202
  57. def OAI.UniversalTensorSquare.sgT155 line 203
  58. def OAI.UniversalTensorSquare.sgFlag155 line 204
  59. lemma OAI.UniversalTensorSquare.sgCert155 line 205
  60. lemma OAI.UniversalTensorSquare.sg155 line 209
  61. def OAI.UniversalTensorSquare.sgB156 line 218
  62. def OAI.UniversalTensorSquare.sgT156 line 219
  63. def OAI.UniversalTensorSquare.sgFlag156 line 220
  64. lemma OAI.UniversalTensorSquare.sgCert156 line 221
  65. lemma OAI.UniversalTensorSquare.sg156 line 225
  66. def OAI.UniversalTensorSquare.sgB157 line 234
  67. def OAI.UniversalTensorSquare.sgT157 line 235
  68. def OAI.UniversalTensorSquare.sgFlag157 line 236
  69. lemma OAI.UniversalTensorSquare.sgCert157 line 237
  70. lemma OAI.UniversalTensorSquare.sg157 line 241
  71. def OAI.UniversalTensorSquare.sgB158 line 250
  72. def OAI.UniversalTensorSquare.sgT158 line 251
  73. def OAI.UniversalTensorSquare.sgFlag158 line 252
  74. lemma OAI.UniversalTensorSquare.sgCert158 line 253
  75. lemma OAI.UniversalTensorSquare.sg158 line 257
  76. def OAI.UniversalTensorSquare.sgB160 line 266
  77. def OAI.UniversalTensorSquare.sgT160 line 267
  78. def OAI.UniversalTensorSquare.sgFlag160 line 268
  79. lemma OAI.UniversalTensorSquare.sgCert160 line 269
  80. lemma OAI.UniversalTensorSquare.sg160 line 273
  81. def OAI.UniversalTensorSquare.sgB163 line 292
  82. def OAI.UniversalTensorSquare.sgT163 line 293
  83. def OAI.UniversalTensorSquare.sgFlag163 line 294
  84. lemma OAI.UniversalTensorSquare.sgCert163 line 295
  85. lemma OAI.UniversalTensorSquare.sg163 line 299
  86. def OAI.UniversalTensorSquare.sgB165 line 308
  87. def OAI.UniversalTensorSquare.sgT165 line 309
  88. def OAI.UniversalTensorSquare.sgFlag165 line 310
  89. lemma OAI.UniversalTensorSquare.sgCert165 line 311
  90. lemma OAI.UniversalTensorSquare.sg165 line 315
  91. def OAI.UniversalTensorSquare.sgB166 line 324
  92. def OAI.UniversalTensorSquare.sgT166 line 325
  93. def OAI.UniversalTensorSquare.sgFlag166 line 326
  94. lemma OAI.UniversalTensorSquare.sgCert166 line 327
  95. lemma OAI.UniversalTensorSquare.sg166 line 331
  96. def OAI.UniversalTensorSquare.sgB167 line 340
  97. def OAI.UniversalTensorSquare.sgT167 line 341
  98. def OAI.UniversalTensorSquare.sgFlag167 line 342
  99. lemma OAI.UniversalTensorSquare.sgCert167 line 343
  100. lemma OAI.UniversalTensorSquare.sg167 line 347
  101. def OAI.UniversalTensorSquare.sgB168 line 356
  102. def OAI.UniversalTensorSquare.sgT168 line 357
  103. def OAI.UniversalTensorSquare.sgFlag168 line 358
  104. lemma OAI.UniversalTensorSquare.sgCert168 line 359
  105. lemma OAI.UniversalTensorSquare.sg168 line 363
  106. def OAI.UniversalTensorSquare.sgB169 line 372
  107. def OAI.UniversalTensorSquare.sgT169 line 373
  108. def OAI.UniversalTensorSquare.sgFlag169 line 374
  109. lemma OAI.UniversalTensorSquare.sgCert169 line 375
  110. lemma OAI.UniversalTensorSquare.sg169 line 379
  111. def OAI.UniversalTensorSquare.sgB171 line 388
  112. def OAI.UniversalTensorSquare.sgT171 line 389
  113. def OAI.UniversalTensorSquare.sgFlag171 line 390
  114. lemma OAI.UniversalTensorSquare.sgCert171 line 391
  115. lemma OAI.UniversalTensorSquare.sg171 line 395
  116. def OAI.UniversalTensorSquare.sgB174 line 404
  117. def OAI.UniversalTensorSquare.sgT174 line 405
  118. def OAI.UniversalTensorSquare.sgFlag174 line 406
  119. lemma OAI.UniversalTensorSquare.sgCert174 line 407
  120. lemma OAI.UniversalTensorSquare.sg174 line 411
  121. def OAI.UniversalTensorSquare.sgB194 line 430
  122. def OAI.UniversalTensorSquare.sgT194 line 431
  123. def OAI.UniversalTensorSquare.sgFlag194 line 432
  124. lemma OAI.UniversalTensorSquare.sgCert194 line 433
  125. lemma OAI.UniversalTensorSquare.sg194 line 437
  126. def OAI.UniversalTensorSquare.sgB195 line 446
  127. def OAI.UniversalTensorSquare.sgT195 line 447
  128. def OAI.UniversalTensorSquare.sgFlag195 line 448
  129. lemma OAI.UniversalTensorSquare.sgCert195 line 449
  130. lemma OAI.UniversalTensorSquare.sg195 line 453
  131. def OAI.UniversalTensorSquare.sgB271 line 462
  132. def OAI.UniversalTensorSquare.sgT271 line 463
  133. def OAI.UniversalTensorSquare.sgFlag271 line 464
  134. lemma OAI.UniversalTensorSquare.sgCert271 line 465
  135. lemma OAI.UniversalTensorSquare.sg271 line 469
  136. def OAI.UniversalTensorSquare.sgB275 line 478
  137. def OAI.UniversalTensorSquare.sgT275 line 479
  138. def OAI.UniversalTensorSquare.sgFlag275 line 480
  139. lemma OAI.UniversalTensorSquare.sgCert275 line 481
  140. lemma OAI.UniversalTensorSquare.sg275 line 485
  141. def OAI.UniversalTensorSquare.sgB285 line 494
  142. def OAI.UniversalTensorSquare.sgT285 line 495
  143. def OAI.UniversalTensorSquare.sgFlag285 line 496
  144. lemma OAI.UniversalTensorSquare.sgCert285 line 497
  145. lemma OAI.UniversalTensorSquare.sg285 line 501
  146. def OAI.UniversalTensorSquare.sgB286 line 510
  147. def OAI.UniversalTensorSquare.sgT286 line 511
  148. def OAI.UniversalTensorSquare.sgFlag286 line 512
  149. lemma OAI.UniversalTensorSquare.sgCert286 line 513
  150. lemma OAI.UniversalTensorSquare.sg286 line 517
  151. def OAI.UniversalTensorSquare.sgB287 line 526
  152. def OAI.UniversalTensorSquare.sgT287 line 527
  153. def OAI.UniversalTensorSquare.sgFlag287 line 528
  154. lemma OAI.UniversalTensorSquare.sgCert287 line 529
  155. lemma OAI.UniversalTensorSquare.sg287 line 533
  156. def OAI.UniversalTensorSquare.sgB295 line 542
  157. def OAI.UniversalTensorSquare.sgT295 line 543
  158. def OAI.UniversalTensorSquare.sgFlag295 line 544
  159. lemma OAI.UniversalTensorSquare.sgCert295 line 545
  160. lemma OAI.UniversalTensorSquare.sg295 line 549
  161. def OAI.UniversalTensorSquare.sgB296 line 568
  162. def OAI.UniversalTensorSquare.sgT296 line 569
  163. def OAI.UniversalTensorSquare.sgFlag296 line 570
  164. lemma OAI.UniversalTensorSquare.sgCert296 line 571
  165. lemma OAI.UniversalTensorSquare.sg296 line 575
  166. def OAI.UniversalTensorSquare.sgB297 line 584
  167. def OAI.UniversalTensorSquare.sgT297 line 585
  168. def OAI.UniversalTensorSquare.sgFlag297 line 586
  169. lemma OAI.UniversalTensorSquare.sgCert297 line 587
  170. lemma OAI.UniversalTensorSquare.sg297 line 591
  171. def OAI.UniversalTensorSquare.sgB300 line 600
  172. def OAI.UniversalTensorSquare.sgT300 line 601
  173. def OAI.UniversalTensorSquare.sgFlag300 line 602
  174. lemma OAI.UniversalTensorSquare.sgCert300 line 603
  175. lemma OAI.UniversalTensorSquare.sg300 line 607
  176. def OAI.UniversalTensorSquare.sgB301 line 616
  177. def OAI.UniversalTensorSquare.sgT301 line 617
  178. def OAI.UniversalTensorSquare.sgFlag301 line 618
  179. lemma OAI.UniversalTensorSquare.sgCert301 line 619
  180. lemma OAI.UniversalTensorSquare.sg301 line 623
  181. def OAI.UniversalTensorSquare.sgB309 line 632
  182. def OAI.UniversalTensorSquare.sgT309 line 633
  183. def OAI.UniversalTensorSquare.sgFlag309 line 634
  184. lemma OAI.UniversalTensorSquare.sgCert309 line 635
  185. lemma OAI.UniversalTensorSquare.sg309 line 639
  186. def OAI.UniversalTensorSquare.sgB310 line 648
  187. def OAI.UniversalTensorSquare.sgT310 line 649
  188. def OAI.UniversalTensorSquare.sgFlag310 line 650
  189. lemma OAI.UniversalTensorSquare.sgCert310 line 651
  190. lemma OAI.UniversalTensorSquare.sg310 line 655
  191. def OAI.UniversalTensorSquare.sgB311 line 664
  192. def OAI.UniversalTensorSquare.sgT311 line 665
  193. def OAI.UniversalTensorSquare.sgFlag311 line 666
  194. lemma OAI.UniversalTensorSquare.sgCert311 line 667
  195. lemma OAI.UniversalTensorSquare.sg311 line 671
  196. def OAI.UniversalTensorSquare.sgB313 line 680
  197. def OAI.UniversalTensorSquare.sgT313 line 681
  198. def OAI.UniversalTensorSquare.sgFlag313 line 682
  199. lemma OAI.UniversalTensorSquare.sgCert313 line 683
  200. lemma OAI.UniversalTensorSquare.sg313 line 687