OAI/GroupTheory/SimpleOvergroups/SourceModel.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.SourceModel.family line 17
  2. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Sigma line 18
  3. abbrev OAI.SimpleFInftyOvergroups.SourceModel.P₂ line 19
  4. abbrev OAI.SimpleFInftyOvergroups.SourceModel.P₃ line 20
  5. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Syntax line 21
  6. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Symbols line 31
  7. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Keys line 32
  8. abbrev OAI.SimpleFInftyOvergroups.SourceModel.code line 37
  9. abbrev OAI.SimpleFInftyOvergroups.SourceModel.search line 38
  10. abbrev OAI.SimpleFInftyOvergroups.SourceModel.wf line 39
  11. theorem OAI.SimpleFInftyOvergroups.SourceModel.bootstrap line 45
  12. def OAI.SimpleFInftyOvergroups.SourceModel.index line 57
  13. abbrev OAI.SimpleFInftyOvergroups.SourceModel.tests line 58
  14. abbrev OAI.SimpleFInftyOvergroups.SourceModel.processor line 60
  15. abbrev OAI.SimpleFInftyOvergroups.SourceModel.value line 62
  16. theorem OAI.SimpleFInftyOvergroups.SourceModel.index_fixed line 64
  17. theorem OAI.SimpleFInftyOvergroups.SourceModel.index_good line 66
  18. theorem OAI.SimpleFInftyOvergroups.SourceModel.index_budget line 68
  19. theorem OAI.SimpleFInftyOvergroups.SourceModel.table_eq line 70
  20. theorem OAI.SimpleFInftyOvergroups.SourceModel.index_stable line 73
  21. theorem OAI.SimpleFInftyOvergroups.SourceModel.tables_short line 77
  22. theorem OAI.SimpleFInftyOvergroups.SourceModel.tables_absorb line 80
  23. theorem OAI.SimpleFInftyOvergroups.SourceModel.certificate line 83
  24. theorem OAI.SimpleFInftyOvergroups.SourceModel.tables_isolate line 88
  25. theorem OAI.SimpleFInftyOvergroups.SourceModel.tables_static line 94
  26. abbrev OAI.SimpleFInftyOvergroups.SourceModel.L line 99
  27. instance OAI.SimpleFInftyOvergroups.SourceModel.lMonoidWithZero line 100
  28. theorem OAI.SimpleFInftyOvergroups.SourceModel.one_ne_zero_L line 103
  29. instance OAI.SimpleFInftyOvergroups.SourceModel.lNontrivial line 106
  30. theorem OAI.SimpleFInftyOvergroups.SourceModel.normal_code line 108
  31. theorem OAI.SimpleFInftyOvergroups.SourceModel.code_eq_iff line 117
  32. theorem OAI.SimpleFInftyOvergroups.SourceModel.code_zero line 126
  33. abbrev OAI.SimpleFInftyOvergroups.SourceModel.KAlphabet line 135
  34. abbrev OAI.SimpleFInftyOvergroups.SourceModel.KMachine line 136
  35. abbrev OAI.SimpleFInftyOvergroups.SourceModel.K line 137
  36. instance OAI.SimpleFInftyOvergroups.SourceModel.kMonoidWithZero line 140
  37. abbrev OAI.SimpleFInftyOvergroups.SourceModel.normalPresentation line 141
  38. abbrev OAI.SimpleFInftyOvergroups.SourceModel.calculus line 143
  39. instance OAI.SimpleFInftyOvergroups.SourceModel.kNontrivial line 145
  40. abbrev OAI.SimpleFInftyOvergroups.SourceModel.B line 149
  41. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Astar line 150
  42. instance OAI.SimpleFInftyOvergroups.SourceModel.bRing line 151
  43. instance OAI.SimpleFInftyOvergroups.SourceModel.bNontrivial line 152
  44. instance OAI.SimpleFInftyOvergroups.SourceModel.bAlgebra line 153
  45. instance OAI.SimpleFInftyOvergroups.SourceModel.aRing line 154
  46. instance OAI.SimpleFInftyOvergroups.SourceModel.aNontrivial line 155
  47. instance OAI.SimpleFInftyOvergroups.SourceModel.aAlgebra line 156
  48. def OAI.SimpleFInftyOvergroups.SourceModel.π line 158
  49. def OAI.SimpleFInftyOvergroups.SourceModel.σ line 160
  50. theorem OAI.SimpleFInftyOvergroups.SourceModel.σ_injective line 162
  51. theorem OAI.SimpleFInftyOvergroups.SourceModel.π_surjective line 163
  52. theorem OAI.SimpleFInftyOvergroups.SourceModel.section_collect line 164
  53. theorem OAI.SimpleFInftyOvergroups.SourceModel.normal_full line 167
  54. theorem OAI.SimpleFInftyOvergroups.SourceModel.value_eq_of_mem line 173
  55. theorem OAI.SimpleFInftyOvergroups.SourceModel.group_value line 177
  56. theorem OAI.SimpleFInftyOvergroups.SourceModel.group_code_eq_iff line 181
  57. def OAI.SimpleFInftyOvergroups.SourceModel.codeG line 187
  58. theorem OAI.SimpleFInftyOvergroups.SourceModel.codeG_injective line 190
  59. abbrev OAI.SimpleFInftyOvergroups.SourceModel.ProdMon line 195
  60. abbrev OAI.SimpleFInftyOvergroups.SourceModel.productEval line 196
  61. theorem OAI.SimpleFInftyOvergroups.SourceModel.product_value line 197
  62. theorem OAI.SimpleFInftyOvergroups.SourceModel.product_code_eq_iff line 201
  63. def OAI.SimpleFInftyOvergroups.SourceModel.codeProduct line 206
  64. theorem OAI.SimpleFInftyOvergroups.SourceModel.codeProduct_injective line 209
  65. theorem OAI.SimpleFInftyOvergroups.SourceModel.codeProduct_zero line 212
  66. def OAI.SimpleFInftyOvergroups.SourceModel.codeProduct₀ line 220
  67. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Acting line 223
  68. abbrev OAI.SimpleFInftyOvergroups.SourceModel.Points line 224
  69. abbrev OAI.SimpleFInftyOvergroups.SourceModel.ActionMon line 226
  70. def OAI.SimpleFInftyOvergroups.SourceModel.actionEval line 227
  71. theorem OAI.SimpleFInftyOvergroups.SourceModel.action_value line 229
  72. theorem OAI.SimpleFInftyOvergroups.SourceModel.action_code_eq_iff line 236
  73. theorem OAI.SimpleFInftyOvergroups.SourceModel.actionEval_surjective line 243
  74. def OAI.SimpleFInftyOvergroups.SourceModel.codeAction line 246
  75. theorem OAI.SimpleFInftyOvergroups.SourceModel.codeAction_injective line 249
  76. theorem OAI.SimpleFInftyOvergroups.SourceModel.codeAction_zero line 252
  77. def OAI.SimpleFInftyOvergroups.SourceModel.codeAction₀ line 261