OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLeaves2.lean

GitHub source file

200 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Leaves 2.

  1. def OAI.UniversalTensorSquare.sgB314 line 16
  2. def OAI.UniversalTensorSquare.sgT314 line 17
  3. def OAI.UniversalTensorSquare.sgFlag314 line 18
  4. lemma OAI.UniversalTensorSquare.sgCert314 line 19
  5. lemma OAI.UniversalTensorSquare.sg314 line 23
  6. def OAI.UniversalTensorSquare.sgB315 line 32
  7. def OAI.UniversalTensorSquare.sgT315 line 33
  8. def OAI.UniversalTensorSquare.sgFlag315 line 34
  9. lemma OAI.UniversalTensorSquare.sgCert315 line 35
  10. lemma OAI.UniversalTensorSquare.sg315 line 39
  11. def OAI.UniversalTensorSquare.sgB319 line 48
  12. def OAI.UniversalTensorSquare.sgT319 line 49
  13. def OAI.UniversalTensorSquare.sgFlag319 line 50
  14. lemma OAI.UniversalTensorSquare.sgCert319 line 51
  15. lemma OAI.UniversalTensorSquare.sg319 line 55
  16. def OAI.UniversalTensorSquare.sgB320 line 64
  17. def OAI.UniversalTensorSquare.sgT320 line 65
  18. def OAI.UniversalTensorSquare.sgFlag320 line 66
  19. lemma OAI.UniversalTensorSquare.sgCert320 line 67
  20. lemma OAI.UniversalTensorSquare.sg320 line 71
  21. def OAI.UniversalTensorSquare.sgB324 line 80
  22. def OAI.UniversalTensorSquare.sgT324 line 81
  23. def OAI.UniversalTensorSquare.sgFlag324 line 82
  24. lemma OAI.UniversalTensorSquare.sgCert324 line 83
  25. lemma OAI.UniversalTensorSquare.sg324 line 87
  26. def OAI.UniversalTensorSquare.sgB348 line 96
  27. def OAI.UniversalTensorSquare.sgT348 line 97
  28. def OAI.UniversalTensorSquare.sgFlag348 line 98
  29. lemma OAI.UniversalTensorSquare.sgCert348 line 99
  30. lemma OAI.UniversalTensorSquare.sg348 line 103
  31. def OAI.UniversalTensorSquare.sgB349 line 112
  32. def OAI.UniversalTensorSquare.sgT349 line 113
  33. def OAI.UniversalTensorSquare.sgFlag349 line 114
  34. lemma OAI.UniversalTensorSquare.sgCert349 line 115
  35. lemma OAI.UniversalTensorSquare.sg349 line 119
  36. def OAI.UniversalTensorSquare.sgB350 line 128
  37. def OAI.UniversalTensorSquare.sgT350 line 129
  38. def OAI.UniversalTensorSquare.sgFlag350 line 130
  39. lemma OAI.UniversalTensorSquare.sgCert350 line 131
  40. lemma OAI.UniversalTensorSquare.sg350 line 135
  41. def OAI.UniversalTensorSquare.sgB352 line 154
  42. def OAI.UniversalTensorSquare.sgT352 line 155
  43. def OAI.UniversalTensorSquare.sgFlag352 line 156
  44. lemma OAI.UniversalTensorSquare.sgCert352 line 157
  45. lemma OAI.UniversalTensorSquare.sg352 line 161
  46. def OAI.UniversalTensorSquare.sgB353 line 170
  47. def OAI.UniversalTensorSquare.sgT353 line 171
  48. def OAI.UniversalTensorSquare.sgFlag353 line 172
  49. lemma OAI.UniversalTensorSquare.sgCert353 line 173
  50. lemma OAI.UniversalTensorSquare.sg353 line 177
  51. def OAI.UniversalTensorSquare.sgB356 line 186
  52. def OAI.UniversalTensorSquare.sgT356 line 187
  53. def OAI.UniversalTensorSquare.sgFlag356 line 188
  54. lemma OAI.UniversalTensorSquare.sgCert356 line 189
  55. lemma OAI.UniversalTensorSquare.sg356 line 193
  56. def OAI.UniversalTensorSquare.sgB357 line 202
  57. def OAI.UniversalTensorSquare.sgT357 line 203
  58. def OAI.UniversalTensorSquare.sgFlag357 line 204
  59. lemma OAI.UniversalTensorSquare.sgCert357 line 205
  60. lemma OAI.UniversalTensorSquare.sg357 line 209
  61. def OAI.UniversalTensorSquare.sgB358 line 218
  62. def OAI.UniversalTensorSquare.sgT358 line 219
  63. def OAI.UniversalTensorSquare.sgFlag358 line 220
  64. lemma OAI.UniversalTensorSquare.sgCert358 line 221
  65. lemma OAI.UniversalTensorSquare.sg358 line 225
  66. def OAI.UniversalTensorSquare.sgB371 line 234
  67. def OAI.UniversalTensorSquare.sgT371 line 235
  68. def OAI.UniversalTensorSquare.sgFlag371 line 236
  69. lemma OAI.UniversalTensorSquare.sgCert371 line 237
  70. lemma OAI.UniversalTensorSquare.sg371 line 241
  71. def OAI.UniversalTensorSquare.sgB372 line 250
  72. def OAI.UniversalTensorSquare.sgT372 line 251
  73. def OAI.UniversalTensorSquare.sgFlag372 line 252
  74. lemma OAI.UniversalTensorSquare.sgCert372 line 253
  75. lemma OAI.UniversalTensorSquare.sg372 line 257
  76. def OAI.UniversalTensorSquare.sgB373 line 266
  77. def OAI.UniversalTensorSquare.sgT373 line 267
  78. def OAI.UniversalTensorSquare.sgFlag373 line 268
  79. lemma OAI.UniversalTensorSquare.sgCert373 line 269
  80. lemma OAI.UniversalTensorSquare.sg373 line 273
  81. def OAI.UniversalTensorSquare.sgB377 line 292
  82. def OAI.UniversalTensorSquare.sgT377 line 293
  83. def OAI.UniversalTensorSquare.sgFlag377 line 294
  84. lemma OAI.UniversalTensorSquare.sgCert377 line 295
  85. lemma OAI.UniversalTensorSquare.sg377 line 299
  86. def OAI.UniversalTensorSquare.sgB378 line 308
  87. def OAI.UniversalTensorSquare.sgT378 line 309
  88. def OAI.UniversalTensorSquare.sgFlag378 line 310
  89. lemma OAI.UniversalTensorSquare.sgCert378 line 311
  90. lemma OAI.UniversalTensorSquare.sg378 line 315
  91. def OAI.UniversalTensorSquare.sgB383 line 324
  92. def OAI.UniversalTensorSquare.sgT383 line 325
  93. def OAI.UniversalTensorSquare.sgFlag383 line 326
  94. lemma OAI.UniversalTensorSquare.sgCert383 line 327
  95. lemma OAI.UniversalTensorSquare.sg383 line 331
  96. def OAI.UniversalTensorSquare.sgB390 line 340
  97. def OAI.UniversalTensorSquare.sgT390 line 341
  98. def OAI.UniversalTensorSquare.sgFlag390 line 342
  99. lemma OAI.UniversalTensorSquare.sgCert390 line 343
  100. lemma OAI.UniversalTensorSquare.sg390 line 347
  101. def OAI.UniversalTensorSquare.sgB394 line 356
  102. def OAI.UniversalTensorSquare.sgT394 line 357
  103. def OAI.UniversalTensorSquare.sgFlag394 line 358
  104. lemma OAI.UniversalTensorSquare.sgCert394 line 359
  105. lemma OAI.UniversalTensorSquare.sg394 line 363
  106. def OAI.UniversalTensorSquare.sgB480 line 372
  107. def OAI.UniversalTensorSquare.sgT480 line 373
  108. def OAI.UniversalTensorSquare.sgFlag480 line 374
  109. lemma OAI.UniversalTensorSquare.sgCert480 line 375
  110. lemma OAI.UniversalTensorSquare.sg480 line 379
  111. def OAI.UniversalTensorSquare.sgB481 line 388
  112. def OAI.UniversalTensorSquare.sgT481 line 389
  113. def OAI.UniversalTensorSquare.sgFlag481 line 390
  114. lemma OAI.UniversalTensorSquare.sgCert481 line 391
  115. lemma OAI.UniversalTensorSquare.sg481 line 395
  116. def OAI.UniversalTensorSquare.sgB482 line 404
  117. def OAI.UniversalTensorSquare.sgT482 line 405
  118. def OAI.UniversalTensorSquare.sgFlag482 line 406
  119. lemma OAI.UniversalTensorSquare.sgCert482 line 407
  120. lemma OAI.UniversalTensorSquare.sg482 line 411
  121. def OAI.UniversalTensorSquare.sgB483 line 430
  122. def OAI.UniversalTensorSquare.sgT483 line 431
  123. def OAI.UniversalTensorSquare.sgFlag483 line 432
  124. lemma OAI.UniversalTensorSquare.sgCert483 line 433
  125. lemma OAI.UniversalTensorSquare.sg483 line 437
  126. def OAI.UniversalTensorSquare.sgB484 line 446
  127. def OAI.UniversalTensorSquare.sgT484 line 447
  128. def OAI.UniversalTensorSquare.sgFlag484 line 448
  129. lemma OAI.UniversalTensorSquare.sgCert484 line 449
  130. lemma OAI.UniversalTensorSquare.sg484 line 453
  131. def OAI.UniversalTensorSquare.sgB487 line 462
  132. def OAI.UniversalTensorSquare.sgT487 line 463
  133. def OAI.UniversalTensorSquare.sgFlag487 line 464
  134. lemma OAI.UniversalTensorSquare.sgCert487 line 465
  135. lemma OAI.UniversalTensorSquare.sg487 line 469
  136. def OAI.UniversalTensorSquare.sgB489 line 478
  137. def OAI.UniversalTensorSquare.sgT489 line 479
  138. def OAI.UniversalTensorSquare.sgFlag489 line 480
  139. lemma OAI.UniversalTensorSquare.sgCert489 line 481
  140. lemma OAI.UniversalTensorSquare.sg489 line 485
  141. def OAI.UniversalTensorSquare.sgB490 line 494
  142. def OAI.UniversalTensorSquare.sgT490 line 495
  143. def OAI.UniversalTensorSquare.sgFlag490 line 496
  144. lemma OAI.UniversalTensorSquare.sgCert490 line 497
  145. lemma OAI.UniversalTensorSquare.sg490 line 501
  146. def OAI.UniversalTensorSquare.sgB495 line 510
  147. def OAI.UniversalTensorSquare.sgT495 line 511
  148. def OAI.UniversalTensorSquare.sgFlag495 line 512
  149. lemma OAI.UniversalTensorSquare.sgCert495 line 513
  150. lemma OAI.UniversalTensorSquare.sg495 line 517
  151. def OAI.UniversalTensorSquare.sgB496 line 526
  152. def OAI.UniversalTensorSquare.sgT496 line 527
  153. def OAI.UniversalTensorSquare.sgFlag496 line 528
  154. lemma OAI.UniversalTensorSquare.sgCert496 line 529
  155. lemma OAI.UniversalTensorSquare.sg496 line 533
  156. def OAI.UniversalTensorSquare.sgB511 line 542
  157. def OAI.UniversalTensorSquare.sgT511 line 543
  158. def OAI.UniversalTensorSquare.sgFlag511 line 544
  159. lemma OAI.UniversalTensorSquare.sgCert511 line 545
  160. lemma OAI.UniversalTensorSquare.sg511 line 549
  161. def OAI.UniversalTensorSquare.sgB513 line 568
  162. def OAI.UniversalTensorSquare.sgT513 line 569
  163. def OAI.UniversalTensorSquare.sgFlag513 line 570
  164. lemma OAI.UniversalTensorSquare.sgCert513 line 571
  165. lemma OAI.UniversalTensorSquare.sg513 line 575
  166. def OAI.UniversalTensorSquare.sgB535 line 584
  167. def OAI.UniversalTensorSquare.sgT535 line 585
  168. def OAI.UniversalTensorSquare.sgFlag535 line 586
  169. lemma OAI.UniversalTensorSquare.sgCert535 line 587
  170. lemma OAI.UniversalTensorSquare.sg535 line 591
  171. def OAI.UniversalTensorSquare.sgB536 line 600
  172. def OAI.UniversalTensorSquare.sgT536 line 601
  173. def OAI.UniversalTensorSquare.sgFlag536 line 602
  174. lemma OAI.UniversalTensorSquare.sgCert536 line 603
  175. lemma OAI.UniversalTensorSquare.sg536 line 607
  176. def OAI.UniversalTensorSquare.sgB537 line 616
  177. def OAI.UniversalTensorSquare.sgT537 line 617
  178. def OAI.UniversalTensorSquare.sgFlag537 line 618
  179. lemma OAI.UniversalTensorSquare.sgCert537 line 619
  180. lemma OAI.UniversalTensorSquare.sg537 line 623
  181. def OAI.UniversalTensorSquare.sgB541 line 632
  182. def OAI.UniversalTensorSquare.sgT541 line 633
  183. def OAI.UniversalTensorSquare.sgFlag541 line 634
  184. lemma OAI.UniversalTensorSquare.sgCert541 line 635
  185. lemma OAI.UniversalTensorSquare.sg541 line 639
  186. def OAI.UniversalTensorSquare.sgB548 line 648
  187. def OAI.UniversalTensorSquare.sgT548 line 649
  188. def OAI.UniversalTensorSquare.sgFlag548 line 650
  189. lemma OAI.UniversalTensorSquare.sgCert548 line 651
  190. lemma OAI.UniversalTensorSquare.sg548 line 655
  191. def OAI.UniversalTensorSquare.sgB549 line 664
  192. def OAI.UniversalTensorSquare.sgT549 line 665
  193. def OAI.UniversalTensorSquare.sgFlag549 line 666
  194. lemma OAI.UniversalTensorSquare.sgCert549 line 667
  195. lemma OAI.UniversalTensorSquare.sg549 line 671
  196. def OAI.UniversalTensorSquare.sgB550 line 680
  197. def OAI.UniversalTensorSquare.sgT550 line 681
  198. def OAI.UniversalTensorSquare.sgFlag550 line 682
  199. lemma OAI.UniversalTensorSquare.sgCert550 line 683
  200. lemma OAI.UniversalTensorSquare.sg550 line 687