OAI/GroupTheory/SimpleOvergroups/ActionMonoid.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceActionMonoid.Generator line 9
  2. abbrev OAI.SourceActionMonoid.Word line 15
  3. inductive OAI.SourceActionMonoid.Relation line 17
  4. abbrev OAI.SourceActionMonoid.M line 31
  5. def OAI.SourceActionMonoid.of line 35
  6. def OAI.SourceActionMonoid.omega line 37
  7. def OAI.SourceActionMonoid.prepend line 39
  8. def OAI.SourceActionMonoid.delete line 40
  9. def OAI.SourceActionMonoid.groupMap line 42
  10. lemma OAI.SourceActionMonoid.of_grp line 47
  11. lemma OAI.SourceActionMonoid.delete_prefix line 49
  12. lemma OAI.SourceActionMonoid.delete_prefix_ne line 52
  13. lemma OAI.SourceActionMonoid.group_prefix line 56
  14. lemma OAI.SourceActionMonoid.delete_group line 59
  15. lemma OAI.SourceActionMonoid.omega_of line 62
  16. lemma OAI.SourceActionMonoid.of_omega line 65
  17. lemma OAI.SourceActionMonoid.omega_mul line 68
  18. lemma OAI.SourceActionMonoid.mul_omega line 76
  19. def OAI.SourceActionMonoid.prefixes line 84
  20. def OAI.SourceActionMonoid.deletions line 86
  21. lemma OAI.SourceActionMonoid.prefixes_nil line 88
  22. lemma OAI.SourceActionMonoid.deletions_nil line 89
  23. lemma OAI.SourceActionMonoid.prefixes_cons line 90
  24. lemma OAI.SourceActionMonoid.deletions_append line 93
  25. lemma OAI.SourceActionMonoid.deletions_cons line 97
  26. def OAI.SourceActionMonoid.normal line 101
  27. lemma OAI.SourceActionMonoid.prepend_normal line 104
  28. lemma OAI.SourceActionMonoid.group_normal_nil line 108
  29. lemma OAI.SourceActionMonoid.group_normal_cons line 112
  30. lemma OAI.SourceActionMonoid.delete_normal_nil line 116
  31. lemma OAI.SourceActionMonoid.delete_normal_cons line 120
  32. lemma OAI.SourceActionMonoid.delete_normal_cons_ne line 124
  33. theorem OAI.SourceActionMonoid.normal_exists line 128
  34. abbrev OAI.SourceActionMonoid.State line 160
  35. def OAI.SourceActionMonoid.headAction line 162
  36. def OAI.SourceActionMonoid.generatorAction line 169
  37. lemma OAI.SourceActionMonoid.end_mul_apply line 178
  38. lemma OAI.SourceActionMonoid.end_one_apply line 180
  39. lemma OAI.SourceActionMonoid.generatorAction_relations line 182
  40. def OAI.SourceActionMonoid.representation line 246
  41. lemma OAI.SourceActionMonoid.representation_of line 249
  42. lemma OAI.SourceActionMonoid.representation_omega line 252
  43. lemma OAI.SourceActionMonoid.representation_group line 255
  44. lemma OAI.SourceActionMonoid.representation_prepend line 258
  45. def OAI.SourceActionMonoid.strip line 261
  46. lemma OAI.SourceActionMonoid.strip_append line 266
  47. lemma OAI.SourceActionMonoid.strip_eq_some_iff line 271
  48. lemma OAI.SourceActionMonoid.representation_prefixes line 283
  49. lemma OAI.SourceActionMonoid.representation_delete_none line 293
  50. lemma OAI.SourceActionMonoid.representation_delete_nil line 296
  51. lemma OAI.SourceActionMonoid.representation_delete_cons line 299
  52. lemma OAI.SourceActionMonoid.representation_deletions_none line 303
  53. lemma OAI.SourceActionMonoid.representation_deletions line 310
  54. lemma OAI.SourceActionMonoid.strip_self line 325
  55. lemma OAI.SourceActionMonoid.representation_normal line 328
  56. lemma OAI.SourceActionMonoid.representation_normal_at line 337
  57. lemma OAI.SourceActionMonoid.normal_ne_zero line 342
  58. lemma OAI.SourceActionMonoid.normal_domain_prefix line 347
  59. theorem OAI.SourceActionMonoid.normal_eq_parameters line 353
  60. theorem OAI.SourceActionMonoid.normal_eq_iff line 367
  61. theorem OAI.SourceActionMonoid.unique_normal_form line 374
  62. theorem OAI.SourceActionMonoid.groupMap_injective line 383
  63. def OAI.SourceActionMonoid.groupUnits line 389
  64. lemma OAI.SourceActionMonoid.groupUnits_val line 391
  65. theorem OAI.SourceActionMonoid.groupUnits_injective line 394
  66. abbrev OAI.SourceActionMonoid.Algorithm.Form line 403
  67. def OAI.SourceActionMonoid.Algorithm.eval line 405
  68. def OAI.SourceActionMonoid.Algorithm.step line 409
  69. lemma OAI.SourceActionMonoid.Algorithm.eval_step line 418
  70. def OAI.SourceActionMonoid.Algorithm.normalize line 446
  71. theorem OAI.SourceActionMonoid.Algorithm.normalize_correct line 450
  72. lemma OAI.SourceActionMonoid.Algorithm.eval_injective line 459
  73. theorem OAI.SourceActionMonoid.Algorithm.word_eq_iff line 475
  74. def OAI.SourceActionMonoid.Algorithm.equalWords line 481
  75. theorem OAI.SourceActionMonoid.Algorithm.equalWords_correct line 484