OAI/GroupTheory/PeriodicGroups/Steinberg/BandFactorization.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.Kernel.left_conjugate_strip_root line 13
  2. lemma OAI.SourceBurnside.Kernel.left_conjugate_strip line 28
  3. lemma OAI.SourceBurnside.Kernel.side_root_normalizes line 37
  4. lemma OAI.SourceBurnside.Kernel.strip_mono line 53
  5. lemma OAI.SourceBurnside.Kernel.blockRoot_mem_subgroup line 58
  6. lemma OAI.SourceBurnside.Kernel.blockRoot_commutes_element line 67
  7. theorem OAI.SourceBurnside.Kernel.block_conjugate_strip line 76
  8. def OAI.SourceBurnside.Kernel.highBand line 136
  9. def OAI.SourceBurnside.Kernel.lowBand line 137
  10. lemma OAI.SourceBurnside.Kernel.bands_disjoint line 138
  11. lemma OAI.SourceBurnside.Kernel.highBand_mono line 143
  12. lemma OAI.SourceBurnside.Kernel.lowBand_mono line 147
  13. def OAI.SourceBurnside.Kernel.bandStrip line 151
  14. lemma OAI.SourceBurnside.Kernel.bandStrip_mono line 153
  15. lemma OAI.SourceBurnside.Kernel.blockRoot_neg line 156
  16. lemma OAI.SourceBurnside.Kernel.band_transport line 159
  17. lemma OAI.SourceBurnside.Kernel.wrap_block_mem line 175
  18. structure OAI.SourceBurnside.Kernel.BlockFactor line 185
  19. def OAI.SourceBurnside.Kernel.wrappedProduct line 189
  20. def OAI.SourceBurnside.Kernel.truncatedProduct line 191
  21. def OAI.SourceBurnside.Kernel.BlockFactor.Bounded line 193
  22. theorem OAI.SourceBurnside.Kernel.band_wrap_collect line 197
  23. theorem OAI.SourceBurnside.Kernel.band_wrap_removal line 229
  24. def OAI.SourceBurnside.Kernel.truncatedShift line 248
  25. def OAI.SourceBurnside.Kernel.cyclicShift line 250
  26. lemma OAI.SourceBurnside.Kernel.truncatedShift_pow line 252
  27. lemma OAI.SourceBurnside.Kernel.cyclicShift_pow line 273
  28. lemma OAI.SourceBurnside.Kernel.truncatedShift_upper line 291
  29. lemma OAI.SourceBurnside.Kernel.truncatedShift_diag line 295
  30. lemma OAI.SourceBurnside.Kernel.numeric_truncatedShift line 298
  31. lemma OAI.SourceBurnside.Kernel.numeric_cyclicShift line 302
  32. lemma OAI.SourceBurnside.Kernel.truncated_eval_monomial line 306
  33. lemma OAI.SourceBurnside.Kernel.cyclic_eval_monomial line 313
  34. lemma OAI.SourceBurnside.Kernel.truncated_eval_outside line 327
  35. lemma OAI.SourceBurnside.Kernel.truncated_eval_band line 336
  36. lemma OAI.SourceBurnside.Kernel.mod_no_wrap_or_low line 341
  37. lemma OAI.SourceBurnside.Kernel.shift_evals_agree_outside line 351
  38. lemma OAI.SourceBurnside.Kernel.cyclic_difference_wrap line 363
  39. def OAI.SourceBurnside.Kernel.rootWord line 378
  40. lemma OAI.SourceBurnside.Kernel.rootWord_append line 379
  41. lemma OAI.SourceBurnside.Kernel.rootWord_inverse line 381
  42. lemma OAI.SourceBurnside.Kernel.exists_rootWord line 388
  43. lemma OAI.SourceBurnside.Kernel.matrixSteinbergEval_x line 402
  44. def OAI.SourceBurnside.Kernel.wrapFactors line 407
  45. lemma OAI.SourceBurnside.Kernel.wrappedProduct_eq line 410
  46. lemma OAI.SourceBurnside.Kernel.truncatedProduct_eq line 420
  47. lemma OAI.SourceBurnside.Kernel.wrapFactors_bounded line 428
  48. theorem OAI.SourceBurnside.Kernel.wrap_removal line 434
  49. def OAI.SourceBurnside.WordAlgebra.Table.gradingRingHom line 456
  50. def OAI.SourceBurnside.WordAlgebra.Table.gradedElement line 464
  51. lemma OAI.SourceBurnside.WordAlgebra.Table.gradedElement_matrix_one line 467
  52. lemma OAI.SourceBurnside.WordAlgebra.Table.gradedElement_one line 471
  53. lemma OAI.SourceBurnside.WordAlgebra.Table.gradedElement_zero line 478
  54. def OAI.SourceBurnside.ConcreteSource.grading line 494
  55. def OAI.SourceBurnside.ConcreteSource.evalZero line 496
  56. def OAI.SourceBurnside.ConcreteSource.evalOne line 497
  57. lemma OAI.SourceBurnside.ConcreteSource.evalOne_grading line 498
  58. lemma OAI.SourceBurnside.ConcreteSource.evalZero_grading line 500
  59. def OAI.SourceBurnside.ConcreteSource.gradedElement line 504
  60. def OAI.SourceBurnside.ConcreteSource.groundElement line 506
  61. lemma OAI.SourceBurnside.ConcreteSource.gradedElement_matrix_one line 507
  62. lemma OAI.SourceBurnside.ConcreteSource.groundElement_matrix_one line 510
  63. lemma OAI.SourceBurnside.ConcreteSource.gradedElement_one line 512
  64. lemma OAI.SourceBurnside.ConcreteSource.gradedElement_zero line 515
  65. lemma OAI.SourceBurnside.Kernel.numerical_matrix_lift line 528
  66. theorem OAI.SourceBurnside.Kernel.stable_uniqueness line 554
  67. def OAI.SourceBurnside.Kernel.coefficientConj line 595
  68. def OAI.SourceBurnside.Kernel.bigBasisUnits line 604
  69. lemma OAI.SourceBurnside.Kernel.scalar_units_conjugates line 606
  70. lemma OAI.SourceBurnside.Kernel.big_conjugates_elementary line 617
  71. theorem OAI.SourceBurnside.Kernel.stable_basis_change line 625