OAI/GroupTheory/PeriodicGroups/Steinberg/MonomialPresentation.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SourceBurnside.one_add_nilpotent_periodic line 10
  2. def OAI.SourceBurnside.MatrixNilKernel line 17
  3. theorem OAI.SourceBurnside.matrix_units_periodic line 21
  4. theorem OAI.SourceBurnside.periodic_of_image_and_kernel line 54
  5. theorem OAI.SourceBurnside.CommutatorCalculus.commute_bracket_right line 66
  6. theorem OAI.SourceBurnside.CommutatorCalculus.commute_bracket_left line 70
  7. theorem OAI.SourceBurnside.CommutatorCalculus.mul_left line 73
  8. theorem OAI.SourceBurnside.CommutatorCalculus.mul_right line 77
  9. theorem OAI.SourceBurnside.CommutatorCalculus.conj_of_commute line 81
  10. theorem OAI.SourceBurnside.CommutatorCalculus.separated line 84
  11. theorem OAI.SourceBurnside.CommutatorCalculus.three_factor line 97
  12. theorem OAI.SourceBurnside.exists_fresh line 140
  13. structure OAI.SourceBurnside.MonomialCompletion.Seed line 152
  14. def OAI.SourceBurnside.MonomialCompletion.middle line 161
  15. theorem OAI.SourceBurnside.MonomialCompletion.middle_ne_row line 164
  16. theorem OAI.SourceBurnside.MonomialCompletion.middle_ne_col line 167
  17. def OAI.SourceBurnside.MonomialCompletion.word line 170
  18. theorem OAI.SourceBurnside.MonomialCompletion.word_short line 178
  19. theorem OAI.SourceBurnside.MonomialCompletion.word_long line 184
  20. abbrev OAI.SourceBurnside.MonomialCompletion.RootWords line 193
  21. def OAI.SourceBurnside.MonomialCompletion.ProductUpTo line 195
  22. def OAI.SourceBurnside.MonomialCompletion.CommuteUpTo line 199
  23. def OAI.SourceBurnside.MonomialCompletion.SquaresUpTo line 203
  24. def OAI.SourceBurnside.MonomialCompletion.Good line 206
  25. theorem OAI.SourceBurnside.MonomialCompletion.base_good line 209
  26. theorem OAI.SourceBurnside.MonomialCompletion.reassociate_of line 223
  27. theorem OAI.SourceBurnside.MonomialCompletion.reassociate line 245
  28. theorem OAI.SourceBurnside.MonomialCompletion.first_cut_independent line 255
  29. theorem OAI.SourceBurnside.MonomialCompletion.first_cut_next line 269
  30. theorem OAI.SourceBurnside.MonomialCompletion.positive_next line 283
  31. theorem OAI.SourceBurnside.MonomialCompletion.commute_next_short line 315
  32. theorem OAI.SourceBurnside.MonomialCompletion.commute_next line 335
  33. theorem OAI.SourceBurnside.MonomialCompletion.bracket_square line 356
  34. theorem OAI.SourceBurnside.MonomialCompletion.squares_next line 370
  35. theorem OAI.SourceBurnside.MonomialCompletion.product_next line 393
  36. theorem OAI.SourceBurnside.MonomialCompletion.good line 446
  37. theorem OAI.SourceBurnside.MonomialCompletion.product line 456
  38. theorem OAI.SourceBurnside.MonomialCompletion.commute line 462
  39. theorem OAI.SourceBurnside.MonomialCompletion.square line 467
  40. abbrev OAI.SourceBurnside.MonomialCompletion.Polynomial line 470
  41. def OAI.SourceBurnside.MonomialCompletion.rootSubgroup line 474
  42. instance OAI.SourceBurnside.MonomialCompletion.rootSubgroup_comm line 477
  43. def OAI.SourceBurnside.MonomialCompletion.rootWord line 483
  44. def OAI.SourceBurnside.MonomialCompletion.coefficient line 486
  45. def OAI.SourceBurnside.MonomialCompletion.poly line 500
  46. theorem OAI.SourceBurnside.MonomialCompletion.poly_zero line 503
  47. theorem OAI.SourceBurnside.MonomialCompletion.poly_add line 506
  48. theorem OAI.SourceBurnside.MonomialCompletion.poly_single line 510
  49. theorem OAI.SourceBurnside.MonomialCompletion.closure_commute line 514
  50. theorem OAI.SourceBurnside.MonomialCompletion.poly_mem line 525
  51. theorem OAI.SourceBurnside.MonomialCompletion.poly_commute line 529
  52. theorem OAI.SourceBurnside.MonomialCompletion.zmod_two_cases line 537
  53. theorem OAI.SourceBurnside.MonomialCompletion.poly_product line 540
  54. def OAI.SourceBurnside.MonomialCompletion.lift line 569
  55. abbrev OAI.SourceBurnside.FiniteSteinbergPresentation.ShortWord line 581
  56. abbrev OAI.SourceBurnside.FiniteSteinbergPresentation.Gen line 582
  57. instance OAI.SourceBurnside.FiniteSteinbergPresentation.root_finite line 584
  58. def OAI.SourceBurnside.FiniteSteinbergPresentation.shortWordMap line 592
  59. instance OAI.SourceBurnside.FiniteSteinbergPresentation.shortWord_finite line 597
  60. def OAI.SourceBurnside.FiniteSteinbergPresentation.gen line 606
  61. inductive OAI.SourceBurnside.FiniteSteinbergPresentation.Rel line 608
  62. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.rel_finite line 617