OAI/RepresentationTheory/UniversalSquare/Semigroup/SemigroupLeaves5.lean

GitHub source file

185 declarations, 0 contain sorry, 0 declared as axioms

Semigroup Leaves 5.

  1. def OAI.UniversalTensorSquare.sgB922 line 16
  2. def OAI.UniversalTensorSquare.sgT922 line 17
  3. def OAI.UniversalTensorSquare.sgFlag922 line 18
  4. lemma OAI.UniversalTensorSquare.sgCert922 line 19
  5. lemma OAI.UniversalTensorSquare.sg922 line 23
  6. def OAI.UniversalTensorSquare.sgB932 line 32
  7. def OAI.UniversalTensorSquare.sgT932 line 33
  8. def OAI.UniversalTensorSquare.sgFlag932 line 34
  9. lemma OAI.UniversalTensorSquare.sgCert932 line 35
  10. lemma OAI.UniversalTensorSquare.sg932 line 39
  11. def OAI.UniversalTensorSquare.sgB939 line 48
  12. def OAI.UniversalTensorSquare.sgT939 line 49
  13. def OAI.UniversalTensorSquare.sgFlag939 line 50
  14. lemma OAI.UniversalTensorSquare.sgCert939 line 51
  15. lemma OAI.UniversalTensorSquare.sg939 line 55
  16. def OAI.UniversalTensorSquare.sgB940 line 64
  17. def OAI.UniversalTensorSquare.sgT940 line 65
  18. def OAI.UniversalTensorSquare.sgFlag940 line 66
  19. lemma OAI.UniversalTensorSquare.sgCert940 line 67
  20. lemma OAI.UniversalTensorSquare.sg940 line 71
  21. def OAI.UniversalTensorSquare.sgB941 line 80
  22. def OAI.UniversalTensorSquare.sgT941 line 81
  23. def OAI.UniversalTensorSquare.sgFlag941 line 82
  24. lemma OAI.UniversalTensorSquare.sgCert941 line 83
  25. lemma OAI.UniversalTensorSquare.sg941 line 87
  26. def OAI.UniversalTensorSquare.sgB942 line 96
  27. def OAI.UniversalTensorSquare.sgT942 line 97
  28. def OAI.UniversalTensorSquare.sgFlag942 line 98
  29. lemma OAI.UniversalTensorSquare.sgCert942 line 99
  30. lemma OAI.UniversalTensorSquare.sg942 line 103
  31. def OAI.UniversalTensorSquare.sgB943 line 112
  32. def OAI.UniversalTensorSquare.sgT943 line 113
  33. def OAI.UniversalTensorSquare.sgFlag943 line 114
  34. lemma OAI.UniversalTensorSquare.sgCert943 line 115
  35. lemma OAI.UniversalTensorSquare.sg943 line 119
  36. def OAI.UniversalTensorSquare.sgB948 line 128
  37. def OAI.UniversalTensorSquare.sgT948 line 129
  38. def OAI.UniversalTensorSquare.sgFlag948 line 130
  39. lemma OAI.UniversalTensorSquare.sgCert948 line 131
  40. lemma OAI.UniversalTensorSquare.sg948 line 135
  41. def OAI.UniversalTensorSquare.sgB949 line 154
  42. def OAI.UniversalTensorSquare.sgT949 line 155
  43. def OAI.UniversalTensorSquare.sgFlag949 line 156
  44. lemma OAI.UniversalTensorSquare.sgCert949 line 157
  45. lemma OAI.UniversalTensorSquare.sg949 line 161
  46. def OAI.UniversalTensorSquare.sgB950 line 170
  47. def OAI.UniversalTensorSquare.sgT950 line 171
  48. def OAI.UniversalTensorSquare.sgFlag950 line 172
  49. lemma OAI.UniversalTensorSquare.sgCert950 line 173
  50. lemma OAI.UniversalTensorSquare.sg950 line 177
  51. def OAI.UniversalTensorSquare.sgB951 line 186
  52. def OAI.UniversalTensorSquare.sgT951 line 187
  53. def OAI.UniversalTensorSquare.sgFlag951 line 188
  54. lemma OAI.UniversalTensorSquare.sgCert951 line 189
  55. lemma OAI.UniversalTensorSquare.sg951 line 193
  56. def OAI.UniversalTensorSquare.sgB958 line 202
  57. def OAI.UniversalTensorSquare.sgT958 line 203
  58. def OAI.UniversalTensorSquare.sgFlag958 line 204
  59. lemma OAI.UniversalTensorSquare.sgCert958 line 205
  60. lemma OAI.UniversalTensorSquare.sg958 line 209
  61. def OAI.UniversalTensorSquare.sgB959 line 218
  62. def OAI.UniversalTensorSquare.sgT959 line 219
  63. def OAI.UniversalTensorSquare.sgFlag959 line 220
  64. lemma OAI.UniversalTensorSquare.sgCert959 line 221
  65. lemma OAI.UniversalTensorSquare.sg959 line 225
  66. def OAI.UniversalTensorSquare.sgB960 line 234
  67. def OAI.UniversalTensorSquare.sgT960 line 235
  68. def OAI.UniversalTensorSquare.sgFlag960 line 236
  69. lemma OAI.UniversalTensorSquare.sgCert960 line 237
  70. lemma OAI.UniversalTensorSquare.sg960 line 241
  71. def OAI.UniversalTensorSquare.sgB961 line 250
  72. def OAI.UniversalTensorSquare.sgT961 line 251
  73. def OAI.UniversalTensorSquare.sgFlag961 line 252
  74. lemma OAI.UniversalTensorSquare.sgCert961 line 253
  75. lemma OAI.UniversalTensorSquare.sg961 line 257
  76. def OAI.UniversalTensorSquare.sgB964 line 266
  77. def OAI.UniversalTensorSquare.sgT964 line 267
  78. def OAI.UniversalTensorSquare.sgFlag964 line 268
  79. lemma OAI.UniversalTensorSquare.sgCert964 line 269
  80. lemma OAI.UniversalTensorSquare.sg964 line 273
  81. def OAI.UniversalTensorSquare.sgB975 line 292
  82. def OAI.UniversalTensorSquare.sgT975 line 293
  83. def OAI.UniversalTensorSquare.sgFlag975 line 294
  84. lemma OAI.UniversalTensorSquare.sgCert975 line 295
  85. lemma OAI.UniversalTensorSquare.sg975 line 299
  86. def OAI.UniversalTensorSquare.sgB976 line 308
  87. def OAI.UniversalTensorSquare.sgT976 line 309
  88. def OAI.UniversalTensorSquare.sgFlag976 line 310
  89. lemma OAI.UniversalTensorSquare.sgCert976 line 311
  90. lemma OAI.UniversalTensorSquare.sg976 line 315
  91. def OAI.UniversalTensorSquare.sgB977 line 324
  92. def OAI.UniversalTensorSquare.sgT977 line 325
  93. def OAI.UniversalTensorSquare.sgFlag977 line 326
  94. lemma OAI.UniversalTensorSquare.sgCert977 line 327
  95. lemma OAI.UniversalTensorSquare.sg977 line 331
  96. def OAI.UniversalTensorSquare.sgB982 line 340
  97. def OAI.UniversalTensorSquare.sgT982 line 341
  98. def OAI.UniversalTensorSquare.sgFlag982 line 342
  99. lemma OAI.UniversalTensorSquare.sgCert982 line 343
  100. lemma OAI.UniversalTensorSquare.sg982 line 347
  101. def OAI.UniversalTensorSquare.sgB998 line 356
  102. def OAI.UniversalTensorSquare.sgT998 line 357
  103. def OAI.UniversalTensorSquare.sgFlag998 line 358
  104. lemma OAI.UniversalTensorSquare.sgCert998 line 359
  105. lemma OAI.UniversalTensorSquare.sg998 line 363
  106. def OAI.UniversalTensorSquare.sgB999 line 372
  107. def OAI.UniversalTensorSquare.sgT999 line 373
  108. def OAI.UniversalTensorSquare.sgFlag999 line 374
  109. lemma OAI.UniversalTensorSquare.sgCert999 line 375
  110. lemma OAI.UniversalTensorSquare.sg999 line 379
  111. def OAI.UniversalTensorSquare.sgB1000 line 388
  112. def OAI.UniversalTensorSquare.sgT1000 line 389
  113. def OAI.UniversalTensorSquare.sgFlag1000 line 390
  114. lemma OAI.UniversalTensorSquare.sgCert1000 line 391
  115. lemma OAI.UniversalTensorSquare.sg1000 line 395
  116. def OAI.UniversalTensorSquare.sgB1001 line 404
  117. def OAI.UniversalTensorSquare.sgT1001 line 405
  118. def OAI.UniversalTensorSquare.sgFlag1001 line 406
  119. lemma OAI.UniversalTensorSquare.sgCert1001 line 407
  120. lemma OAI.UniversalTensorSquare.sg1001 line 411
  121. def OAI.UniversalTensorSquare.sgB1006 line 430
  122. def OAI.UniversalTensorSquare.sgT1006 line 431
  123. def OAI.UniversalTensorSquare.sgFlag1006 line 432
  124. lemma OAI.UniversalTensorSquare.sgCert1006 line 433
  125. lemma OAI.UniversalTensorSquare.sg1006 line 437
  126. def OAI.UniversalTensorSquare.sgB1007 line 446
  127. def OAI.UniversalTensorSquare.sgT1007 line 447
  128. def OAI.UniversalTensorSquare.sgFlag1007 line 448
  129. lemma OAI.UniversalTensorSquare.sgCert1007 line 449
  130. lemma OAI.UniversalTensorSquare.sg1007 line 453
  131. def OAI.UniversalTensorSquare.sgB1008 line 462
  132. def OAI.UniversalTensorSquare.sgT1008 line 463
  133. def OAI.UniversalTensorSquare.sgFlag1008 line 464
  134. lemma OAI.UniversalTensorSquare.sgCert1008 line 465
  135. lemma OAI.UniversalTensorSquare.sg1008 line 469
  136. def OAI.UniversalTensorSquare.sgB1015 line 478
  137. def OAI.UniversalTensorSquare.sgT1015 line 479
  138. def OAI.UniversalTensorSquare.sgFlag1015 line 480
  139. lemma OAI.UniversalTensorSquare.sgCert1015 line 481
  140. lemma OAI.UniversalTensorSquare.sg1015 line 485
  141. def OAI.UniversalTensorSquare.sgB1016 line 494
  142. def OAI.UniversalTensorSquare.sgT1016 line 495
  143. def OAI.UniversalTensorSquare.sgFlag1016 line 496
  144. lemma OAI.UniversalTensorSquare.sgCert1016 line 497
  145. lemma OAI.UniversalTensorSquare.sg1016 line 501
  146. def OAI.UniversalTensorSquare.sgB1023 line 510
  147. def OAI.UniversalTensorSquare.sgT1023 line 511
  148. def OAI.UniversalTensorSquare.sgFlag1023 line 512
  149. lemma OAI.UniversalTensorSquare.sgCert1023 line 513
  150. lemma OAI.UniversalTensorSquare.sg1023 line 517
  151. def OAI.UniversalTensorSquare.sgB1032 line 526
  152. def OAI.UniversalTensorSquare.sgT1032 line 527
  153. def OAI.UniversalTensorSquare.sgFlag1032 line 528
  154. lemma OAI.UniversalTensorSquare.sgCert1032 line 529
  155. lemma OAI.UniversalTensorSquare.sg1032 line 533
  156. def OAI.UniversalTensorSquare.sgB1033 line 542
  157. def OAI.UniversalTensorSquare.sgT1033 line 543
  158. def OAI.UniversalTensorSquare.sgFlag1033 line 544
  159. lemma OAI.UniversalTensorSquare.sgCert1033 line 545
  160. lemma OAI.UniversalTensorSquare.sg1033 line 549
  161. def OAI.UniversalTensorSquare.sgB1038 line 568
  162. def OAI.UniversalTensorSquare.sgT1038 line 569
  163. def OAI.UniversalTensorSquare.sgFlag1038 line 570
  164. lemma OAI.UniversalTensorSquare.sgCert1038 line 571
  165. lemma OAI.UniversalTensorSquare.sg1038 line 575
  166. def OAI.UniversalTensorSquare.sgB1040 line 584
  167. def OAI.UniversalTensorSquare.sgT1040 line 585
  168. def OAI.UniversalTensorSquare.sgFlag1040 line 586
  169. lemma OAI.UniversalTensorSquare.sgCert1040 line 587
  170. lemma OAI.UniversalTensorSquare.sg1040 line 591
  171. def OAI.UniversalTensorSquare.sgB1063 line 600
  172. def OAI.UniversalTensorSquare.sgT1063 line 601
  173. def OAI.UniversalTensorSquare.sgFlag1063 line 602
  174. lemma OAI.UniversalTensorSquare.sgCert1063 line 603
  175. lemma OAI.UniversalTensorSquare.sg1063 line 607
  176. def OAI.UniversalTensorSquare.sgB1064 line 616
  177. def OAI.UniversalTensorSquare.sgT1064 line 617
  178. def OAI.UniversalTensorSquare.sgFlag1064 line 618
  179. lemma OAI.UniversalTensorSquare.sgCert1064 line 619
  180. lemma OAI.UniversalTensorSquare.sg1064 line 623
  181. def OAI.UniversalTensorSquare.sgB1065 line 632
  182. def OAI.UniversalTensorSquare.sgT1065 line 633
  183. def OAI.UniversalTensorSquare.sgFlag1065 line 634
  184. lemma OAI.UniversalTensorSquare.sgCert1065 line 635
  185. lemma OAI.UniversalTensorSquare.sg1065 line 639