OAI/GroupTheory/PeriodicGroups/Steinberg/PresentationModel.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.SourceMachine.MachineHierarchy.Token line 14
  2. instance OAI.SourceBurnside.SourceMachine.MachineHierarchy.token_finite line 15
  3. instance OAI.SourceBurnside.SourceMachine.MachineHierarchy.token_fintype line 16
  4. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.normal line 17
  5. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.normal_spec line 19
  6. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.normal_word line 24
  7. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.letters line 29
  8. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.eval_letters line 31
  9. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.cut_reduction line 35
  10. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.LetterVanish line 104
  11. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.ChunkVanish line 107
  12. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.cut_step line 111
  13. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.automaton_step line 118
  14. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.direct_step line 133
  15. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.all_letter_tests line 142
  16. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.all_chunk_tests line 181
  17. structure OAI.SourceBurnside.Root line 189

    Also declared: ComparatorChallenges/PeriodicGroup.lean:9 (same declaration text).

  18. abbrev OAI.SourceBurnside.Generator line 195

    Also declared: ComparatorChallenges/PeriodicGroup.lean:15 (same declaration text).

  19. def OAI.SourceBurnside.bracket line 197

    Also declared: ComparatorChallenges/PeriodicGroup.lean:17 (same declaration text).

  20. def OAI.SourceBurnside.letter line 199

    Also declared: ComparatorChallenges/PeriodicGroup.lean:19 (same declaration text).

  21. inductive OAI.SourceBurnside.SteinbergRel line 202

    Also declared: ComparatorChallenges/PeriodicGroup.lean:22 (same declaration text).

  22. def OAI.SourceBurnside.Steinberg line 213

    Also declared: ComparatorChallenges/PeriodicGroup.lean:33 (same declaration text).

  23. def OAI.SourceBurnside.Periodic line 217

    Also declared: ComparatorChallenges/PeriodicGroup.lean:37 (same declaration text).

  24. def OAI.SourceBurnside.MainStatement line 219

    Also declared: ComparatorChallenges/PeriodicGroup.lean:39 (same declaration text).

  25. def OAI.SourceBurnside.BurnsideStatement line 224

    Also declared: ComparatorChallenges/PeriodicGroup.lean:44 (same declaration text).

  26. theorem OAI.SourceBurnside.map_bracket line 231
  27. theorem OAI.SourceBurnside.bracket_eq_one_iff line 235
  28. def OAI.SourceBurnside.Steinberg.x line 244
  29. theorem OAI.SourceBurnside.Steinberg.x_add line 246
  30. theorem OAI.SourceBurnside.Steinberg.x_zero line 249
  31. theorem OAI.SourceBurnside.Steinberg.x_neg line 254
  32. theorem OAI.SourceBurnside.Steinberg.x_commute line 258
  33. theorem OAI.SourceBurnside.Steinberg.x_mul line 265
  34. def OAI.SourceBurnside.Steinberg.lift line 272
  35. theorem OAI.SourceBurnside.Steinberg.lift_x line 288
  36. theorem OAI.SourceBurnside.Steinberg.hom_ext line 292
  37. theorem OAI.SourceBurnside.Steinberg.closure_range_x line 298
  38. def OAI.SourceBurnside.Steinberg.map line 301
  39. theorem OAI.SourceBurnside.Steinberg.map_x line 305
  40. theorem OAI.SourceBurnside.burnside_of_main line 310
  41. def OAI.SourceBurnside.Elementary.e line 322
  42. theorem OAI.SourceBurnside.Elementary.coe_e line 328
  43. theorem OAI.SourceBurnside.Elementary.e_add line 331
  44. theorem OAI.SourceBurnside.Elementary.e_zero line 335
  45. theorem OAI.SourceBurnside.Elementary.e_inv line 339
  46. theorem OAI.SourceBurnside.Elementary.e_commute line 343
  47. theorem OAI.SourceBurnside.Elementary.e_mul line 352
  48. def OAI.SourceBurnside.Elementary.representation line 361
  49. theorem OAI.SourceBurnside.Elementary.representation_x line 364
  50. theorem OAI.SourceBurnside.Elementary.e_injective line 367
  51. theorem OAI.SourceBurnside.Elementary.x_injective line 372
  52. theorem OAI.SourceBurnside.Elementary.steinberg_infinite line 377