OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLeaves3.lean

GitHub source file

200 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Leaves 3.

  1. def OAI.UniversalTensorSquare.sgB551 line 16
  2. def OAI.UniversalTensorSquare.sgT551 line 17
  3. def OAI.UniversalTensorSquare.sgFlag551 line 18
  4. lemma OAI.UniversalTensorSquare.sgCert551 line 19
  5. lemma OAI.UniversalTensorSquare.sg551 line 23
  6. def OAI.UniversalTensorSquare.sgB552 line 32
  7. def OAI.UniversalTensorSquare.sgT552 line 33
  8. def OAI.UniversalTensorSquare.sgFlag552 line 34
  9. lemma OAI.UniversalTensorSquare.sgCert552 line 35
  10. lemma OAI.UniversalTensorSquare.sg552 line 39
  11. def OAI.UniversalTensorSquare.sgB553 line 48
  12. def OAI.UniversalTensorSquare.sgT553 line 49
  13. def OAI.UniversalTensorSquare.sgFlag553 line 50
  14. lemma OAI.UniversalTensorSquare.sgCert553 line 51
  15. lemma OAI.UniversalTensorSquare.sg553 line 55
  16. def OAI.UniversalTensorSquare.sgB559 line 64
  17. def OAI.UniversalTensorSquare.sgT559 line 65
  18. def OAI.UniversalTensorSquare.sgFlag559 line 66
  19. lemma OAI.UniversalTensorSquare.sgCert559 line 67
  20. lemma OAI.UniversalTensorSquare.sg559 line 71
  21. def OAI.UniversalTensorSquare.sgB561 line 80
  22. def OAI.UniversalTensorSquare.sgT561 line 81
  23. def OAI.UniversalTensorSquare.sgFlag561 line 82
  24. lemma OAI.UniversalTensorSquare.sgCert561 line 83
  25. lemma OAI.UniversalTensorSquare.sg561 line 87
  26. def OAI.UniversalTensorSquare.sgB562 line 96
  27. def OAI.UniversalTensorSquare.sgT562 line 97
  28. def OAI.UniversalTensorSquare.sgFlag562 line 98
  29. lemma OAI.UniversalTensorSquare.sgCert562 line 99
  30. lemma OAI.UniversalTensorSquare.sg562 line 103
  31. def OAI.UniversalTensorSquare.sgB563 line 112
  32. def OAI.UniversalTensorSquare.sgT563 line 113
  33. def OAI.UniversalTensorSquare.sgFlag563 line 114
  34. lemma OAI.UniversalTensorSquare.sgCert563 line 115
  35. lemma OAI.UniversalTensorSquare.sg563 line 119
  36. def OAI.UniversalTensorSquare.sgB564 line 128
  37. def OAI.UniversalTensorSquare.sgT564 line 129
  38. def OAI.UniversalTensorSquare.sgFlag564 line 130
  39. lemma OAI.UniversalTensorSquare.sgCert564 line 131
  40. lemma OAI.UniversalTensorSquare.sg564 line 135
  41. def OAI.UniversalTensorSquare.sgB565 line 154
  42. def OAI.UniversalTensorSquare.sgT565 line 155
  43. def OAI.UniversalTensorSquare.sgFlag565 line 156
  44. lemma OAI.UniversalTensorSquare.sgCert565 line 157
  45. lemma OAI.UniversalTensorSquare.sg565 line 161
  46. def OAI.UniversalTensorSquare.sgB569 line 170
  47. def OAI.UniversalTensorSquare.sgT569 line 171
  48. def OAI.UniversalTensorSquare.sgFlag569 line 172
  49. lemma OAI.UniversalTensorSquare.sgCert569 line 173
  50. lemma OAI.UniversalTensorSquare.sg569 line 177
  51. def OAI.UniversalTensorSquare.sgB570 line 186
  52. def OAI.UniversalTensorSquare.sgT570 line 187
  53. def OAI.UniversalTensorSquare.sgFlag570 line 188
  54. lemma OAI.UniversalTensorSquare.sgCert570 line 189
  55. lemma OAI.UniversalTensorSquare.sg570 line 193
  56. def OAI.UniversalTensorSquare.sgB575 line 202
  57. def OAI.UniversalTensorSquare.sgT575 line 203
  58. def OAI.UniversalTensorSquare.sgFlag575 line 204
  59. lemma OAI.UniversalTensorSquare.sgCert575 line 205
  60. lemma OAI.UniversalTensorSquare.sg575 line 209
  61. def OAI.UniversalTensorSquare.sgB577 line 218
  62. def OAI.UniversalTensorSquare.sgT577 line 219
  63. def OAI.UniversalTensorSquare.sgFlag577 line 220
  64. lemma OAI.UniversalTensorSquare.sgCert577 line 221
  65. lemma OAI.UniversalTensorSquare.sg577 line 225
  66. def OAI.UniversalTensorSquare.sgB578 line 234
  67. def OAI.UniversalTensorSquare.sgT578 line 235
  68. def OAI.UniversalTensorSquare.sgFlag578 line 236
  69. lemma OAI.UniversalTensorSquare.sgCert578 line 237
  70. lemma OAI.UniversalTensorSquare.sg578 line 241
  71. def OAI.UniversalTensorSquare.sgB579 line 250
  72. def OAI.UniversalTensorSquare.sgT579 line 251
  73. def OAI.UniversalTensorSquare.sgFlag579 line 252
  74. lemma OAI.UniversalTensorSquare.sgCert579 line 253
  75. lemma OAI.UniversalTensorSquare.sg579 line 257
  76. def OAI.UniversalTensorSquare.sgB580 line 266
  77. def OAI.UniversalTensorSquare.sgT580 line 267
  78. def OAI.UniversalTensorSquare.sgFlag580 line 268
  79. lemma OAI.UniversalTensorSquare.sgCert580 line 269
  80. lemma OAI.UniversalTensorSquare.sg580 line 273
  81. def OAI.UniversalTensorSquare.sgB581 line 292
  82. def OAI.UniversalTensorSquare.sgT581 line 293
  83. def OAI.UniversalTensorSquare.sgFlag581 line 294
  84. lemma OAI.UniversalTensorSquare.sgCert581 line 295
  85. lemma OAI.UniversalTensorSquare.sg581 line 299
  86. def OAI.UniversalTensorSquare.sgB582 line 308
  87. def OAI.UniversalTensorSquare.sgT582 line 309
  88. def OAI.UniversalTensorSquare.sgFlag582 line 310
  89. lemma OAI.UniversalTensorSquare.sgCert582 line 311
  90. lemma OAI.UniversalTensorSquare.sg582 line 315
  91. def OAI.UniversalTensorSquare.sgB583 line 324
  92. def OAI.UniversalTensorSquare.sgT583 line 325
  93. def OAI.UniversalTensorSquare.sgFlag583 line 326
  94. lemma OAI.UniversalTensorSquare.sgCert583 line 327
  95. lemma OAI.UniversalTensorSquare.sg583 line 331
  96. def OAI.UniversalTensorSquare.sgB584 line 340
  97. def OAI.UniversalTensorSquare.sgT584 line 341
  98. def OAI.UniversalTensorSquare.sgFlag584 line 342
  99. lemma OAI.UniversalTensorSquare.sgCert584 line 343
  100. lemma OAI.UniversalTensorSquare.sg584 line 347
  101. def OAI.UniversalTensorSquare.sgB614 line 356
  102. def OAI.UniversalTensorSquare.sgT614 line 357
  103. def OAI.UniversalTensorSquare.sgFlag614 line 358
  104. lemma OAI.UniversalTensorSquare.sgCert614 line 359
  105. lemma OAI.UniversalTensorSquare.sg614 line 363
  106. def OAI.UniversalTensorSquare.sgB615 line 372
  107. def OAI.UniversalTensorSquare.sgT615 line 373
  108. def OAI.UniversalTensorSquare.sgFlag615 line 374
  109. lemma OAI.UniversalTensorSquare.sgCert615 line 375
  110. lemma OAI.UniversalTensorSquare.sg615 line 379
  111. def OAI.UniversalTensorSquare.sgB616 line 388
  112. def OAI.UniversalTensorSquare.sgT616 line 389
  113. def OAI.UniversalTensorSquare.sgFlag616 line 390
  114. lemma OAI.UniversalTensorSquare.sgCert616 line 391
  115. lemma OAI.UniversalTensorSquare.sg616 line 395
  116. def OAI.UniversalTensorSquare.sgB621 line 404
  117. def OAI.UniversalTensorSquare.sgT621 line 405
  118. def OAI.UniversalTensorSquare.sgFlag621 line 406
  119. lemma OAI.UniversalTensorSquare.sgCert621 line 407
  120. lemma OAI.UniversalTensorSquare.sg621 line 411
  121. def OAI.UniversalTensorSquare.sgB636 line 430
  122. def OAI.UniversalTensorSquare.sgT636 line 431
  123. def OAI.UniversalTensorSquare.sgFlag636 line 432
  124. lemma OAI.UniversalTensorSquare.sgCert636 line 433
  125. lemma OAI.UniversalTensorSquare.sg636 line 437
  126. def OAI.UniversalTensorSquare.sgB637 line 446
  127. def OAI.UniversalTensorSquare.sgT637 line 447
  128. def OAI.UniversalTensorSquare.sgFlag637 line 448
  129. lemma OAI.UniversalTensorSquare.sgCert637 line 449
  130. lemma OAI.UniversalTensorSquare.sg637 line 453
  131. def OAI.UniversalTensorSquare.sgB640 line 462
  132. def OAI.UniversalTensorSquare.sgT640 line 463
  133. def OAI.UniversalTensorSquare.sgFlag640 line 464
  134. lemma OAI.UniversalTensorSquare.sgCert640 line 465
  135. lemma OAI.UniversalTensorSquare.sg640 line 469
  136. def OAI.UniversalTensorSquare.sgB641 line 478
  137. def OAI.UniversalTensorSquare.sgT641 line 479
  138. def OAI.UniversalTensorSquare.sgFlag641 line 480
  139. lemma OAI.UniversalTensorSquare.sgCert641 line 481
  140. lemma OAI.UniversalTensorSquare.sg641 line 485
  141. def OAI.UniversalTensorSquare.sgB759 line 494
  142. def OAI.UniversalTensorSquare.sgT759 line 495
  143. def OAI.UniversalTensorSquare.sgFlag759 line 496
  144. lemma OAI.UniversalTensorSquare.sgCert759 line 497
  145. lemma OAI.UniversalTensorSquare.sg759 line 501
  146. def OAI.UniversalTensorSquare.sgB765 line 510
  147. def OAI.UniversalTensorSquare.sgT765 line 511
  148. def OAI.UniversalTensorSquare.sgFlag765 line 512
  149. lemma OAI.UniversalTensorSquare.sgCert765 line 513
  150. lemma OAI.UniversalTensorSquare.sg765 line 517
  151. def OAI.UniversalTensorSquare.sgB767 line 526
  152. def OAI.UniversalTensorSquare.sgT767 line 527
  153. def OAI.UniversalTensorSquare.sgFlag767 line 528
  154. lemma OAI.UniversalTensorSquare.sgCert767 line 529
  155. lemma OAI.UniversalTensorSquare.sg767 line 533
  156. def OAI.UniversalTensorSquare.sgB768 line 542
  157. def OAI.UniversalTensorSquare.sgT768 line 543
  158. def OAI.UniversalTensorSquare.sgFlag768 line 544
  159. lemma OAI.UniversalTensorSquare.sgCert768 line 545
  160. lemma OAI.UniversalTensorSquare.sg768 line 549
  161. def OAI.UniversalTensorSquare.sgB790 line 568
  162. def OAI.UniversalTensorSquare.sgT790 line 569
  163. def OAI.UniversalTensorSquare.sgFlag790 line 570
  164. lemma OAI.UniversalTensorSquare.sgCert790 line 571
  165. lemma OAI.UniversalTensorSquare.sg790 line 575
  166. def OAI.UniversalTensorSquare.sgB791 line 584
  167. def OAI.UniversalTensorSquare.sgT791 line 585
  168. def OAI.UniversalTensorSquare.sgFlag791 line 586
  169. lemma OAI.UniversalTensorSquare.sgCert791 line 587
  170. lemma OAI.UniversalTensorSquare.sg791 line 591
  171. def OAI.UniversalTensorSquare.sgB792 line 600
  172. def OAI.UniversalTensorSquare.sgT792 line 601
  173. def OAI.UniversalTensorSquare.sgFlag792 line 602
  174. lemma OAI.UniversalTensorSquare.sgCert792 line 603
  175. lemma OAI.UniversalTensorSquare.sg792 line 607
  176. def OAI.UniversalTensorSquare.sgB796 line 616
  177. def OAI.UniversalTensorSquare.sgT796 line 617
  178. def OAI.UniversalTensorSquare.sgFlag796 line 618
  179. lemma OAI.UniversalTensorSquare.sgCert796 line 619
  180. lemma OAI.UniversalTensorSquare.sg796 line 623
  181. def OAI.UniversalTensorSquare.sgB808 line 632
  182. def OAI.UniversalTensorSquare.sgT808 line 633
  183. def OAI.UniversalTensorSquare.sgFlag808 line 634
  184. lemma OAI.UniversalTensorSquare.sgCert808 line 635
  185. lemma OAI.UniversalTensorSquare.sg808 line 639
  186. def OAI.UniversalTensorSquare.sgB809 line 648
  187. def OAI.UniversalTensorSquare.sgT809 line 649
  188. def OAI.UniversalTensorSquare.sgFlag809 line 650
  189. lemma OAI.UniversalTensorSquare.sgCert809 line 651
  190. lemma OAI.UniversalTensorSquare.sg809 line 655
  191. def OAI.UniversalTensorSquare.sgB814 line 664
  192. def OAI.UniversalTensorSquare.sgT814 line 665
  193. def OAI.UniversalTensorSquare.sgFlag814 line 666
  194. lemma OAI.UniversalTensorSquare.sgCert814 line 667
  195. lemma OAI.UniversalTensorSquare.sg814 line 671
  196. def OAI.UniversalTensorSquare.sgB816 line 680
  197. def OAI.UniversalTensorSquare.sgT816 line 681
  198. def OAI.UniversalTensorSquare.sgFlag816 line 682
  199. lemma OAI.UniversalTensorSquare.sgCert816 line 683
  200. lemma OAI.UniversalTensorSquare.sg816 line 687