OAI/GroupTheory/PeriodicGroups/Steinberg/CoefficientQuotients.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.FiniteSteinbergPresentation.Group line 12
  2. instance OAI.SourceBurnside.FiniteSteinbergPresentation.finitelyPresented line 14
  3. def OAI.SourceBurnside.FiniteSteinbergPresentation.seed line 18
  4. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.seed_short line 41
  5. def OAI.SourceBurnside.FiniteSteinbergPresentation.monomial line 44
  6. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.monomial_append line 46
  7. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.monomial_add_self line 50
  8. def OAI.SourceBurnside.FiniteSteinbergPresentation.toSteinberg line 54
  9. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.toSteinberg_of line 68
  10. def OAI.SourceBurnside.FiniteSteinbergPresentation.fromSteinberg line 72
  11. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.fromSteinberg_x line 75
  12. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.toSteinberg_seed line 79
  13. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.toSteinberg_word line 83
  14. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.toSteinberg_poly line 97
  15. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.from_to line 108
  16. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.to_from line 119
  17. def OAI.SourceBurnside.FiniteSteinbergPresentation.equiv line 125
  18. theorem OAI.SourceBurnside.FiniteSteinbergPresentation.free_finitelyPresented line 132
  19. def OAI.SourceBurnside.SteinbergQuotient.killedIdeal line 142
  20. theorem OAI.SourceBurnside.SteinbergQuotient.mem_killedIdeal line 159
  21. def OAI.SourceBurnside.SteinbergQuotient.rootRelations line 166
  22. abbrev OAI.SourceBurnside.SteinbergQuotient.normal line 168
  23. abbrev OAI.SourceBurnside.SteinbergQuotient.Quot line 170
  24. abbrev OAI.SourceBurnside.SteinbergQuotient.coeffIdeal line 172
  25. abbrev OAI.SourceBurnside.SteinbergQuotient.Coeff line 174
  26. abbrev OAI.SourceBurnside.SteinbergQuotient.proj line 176
  27. theorem OAI.SourceBurnside.SteinbergQuotient.killed line 178
  28. def OAI.SourceBurnside.SteinbergQuotient.quotientRoot line 189
  29. theorem OAI.SourceBurnside.SteinbergQuotient.quotientRoot_mk line 196
  30. def OAI.SourceBurnside.SteinbergQuotient.fromCoeff line 199
  31. theorem OAI.SourceBurnside.SteinbergQuotient.fromCoeff_x line 220
  32. theorem OAI.SourceBurnside.SteinbergQuotient.normal_le_ker line 226
  33. def OAI.SourceBurnside.SteinbergQuotient.toCoeff line 236
  34. theorem OAI.SourceBurnside.SteinbergQuotient.toCoeff_proj line 239
  35. theorem OAI.SourceBurnside.SteinbergQuotient.fromCoeff_comp_toCoeff line 242
  36. theorem OAI.SourceBurnside.SteinbergQuotient.toCoeff_comp_fromCoeff line 254
  37. def OAI.SourceBurnside.SteinbergQuotient.equiv line 263
  38. theorem OAI.SourceBurnside.SteinbergQuotient.rootRelations_finite line 270
  39. theorem OAI.SourceBurnside.SteinbergQuotient.normal_finitelyGenerated line 282
  40. theorem OAI.SourceBurnside.SteinbergQuotient.finitelyPresented line 286
  41. theorem OAI.SourceBurnside.steinberg_finitelyPresented line 295
  42. def OAI.SourceBurnside.WordAlgebra.Table.polynomialCoefficients line 309
  43. lemma OAI.SourceBurnside.WordAlgebra.Table.polynomialCoefficients_word line 331
  44. def OAI.SourceBurnside.MatrixTests.polynomialMatrix line 344
  45. lemma OAI.SourceBurnside.MatrixTests.polynomialMatrix_monomial line 347
  46. lemma OAI.SourceBurnside.MatrixTests.polynomialMatrix_coeff line 353
  47. lemma OAI.SourceBurnside.MatrixTests.polynomialMatrix_injective line 361
  48. lemma OAI.SourceBurnside.MatrixTests.eval_monomial_one line 374
  49. lemma OAI.SourceBurnside.MatrixTests.chunkSum_monomial line 384
  50. lemma OAI.SourceBurnside.MatrixTests.polynomial_tensor line 406
  51. lemma OAI.SourceBurnside.MatrixTests.map_chunkSum line 423
  52. lemma OAI.SourceBurnside.MatrixTests.map_test_polynomial line 427
  53. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.word_matrix_sum_nilpotent line 456
  54. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.positiveSpan line 492
  55. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.positive_matrix_nilpotent line 497
  56. def OAI.SourceBurnside.WordAlgebra.Table.augWords line 526
  57. lemma OAI.SourceBurnside.WordAlgebra.Table.augWords_spec line 527
  58. def OAI.SourceBurnside.WordAlgebra.Table.augmentation line 534
  59. lemma OAI.SourceBurnside.WordAlgebra.Table.augmentation_word line 550
  60. lemma OAI.SourceBurnside.WordAlgebra.Table.quotient_smul line 554
  61. lemma OAI.SourceBurnside.WordAlgebra.Table.sub_augmentation_mem line 557
  62. lemma OAI.SourceBurnside.WordAlgebra.Table.kernel_mem line 579
  63. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.table_homogeneous line 592
  64. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.table_zero_nonempty line 594
  65. def OAI.SourceBurnside.SourceMachine.MachineHierarchy.augmentation line 599
  66. lemma OAI.SourceBurnside.SourceMachine.MachineHierarchy.augmentation_kernel_positive line 601
  67. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.matrixNilKernel line 612
  68. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.matrix_periodic line 619
  69. def OAI.SourceBurnside.FiniteTable.Codec.boundedWords line 632
  70. lemma OAI.SourceBurnside.FiniteTable.Codec.finite_boundedWords line 634
  71. lemma OAI.SourceBurnside.FiniteTable.Codec.mem_boundedWords line 635
  72. lemma OAI.SourceBurnside.FiniteTable.Codec.finite_algebraTable_relations line 640
  73. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.steinberg_finitely_presented line 664
  74. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.steinberg_infinite line 668
  75. theorem OAI.SourceBurnside.SourceMachine.MachineHierarchy.infinite_and_fp line 673
  76. def OAI.SourceBurnside.ConcreteSource.dilation line 683
  77. lemma OAI.SourceBurnside.ConcreteSource.dilation_two line 684
  78. lemma OAI.SourceBurnside.ConcreteSource.dilation_large line 685
  79. def OAI.SourceBurnside.ConcreteSource.machine line 686
  80. def OAI.SourceBurnside.ConcreteSource.height line 687
  81. abbrev OAI.SourceBurnside.ConcreteSource.R line 689
  82. def OAI.SourceBurnside.ConcreteSource.augmentation line 690
  83. instance OAI.SourceBurnside.ConcreteSource.ring_infinite line 691
  84. instance OAI.SourceBurnside.ConcreteSource.characteristic line 692
  85. theorem OAI.SourceBurnside.ConcreteSource.steinberg_infinite line 695
  86. theorem OAI.SourceBurnside.ConcreteSource.steinberg_finitely_presented line 697
  87. theorem OAI.SourceBurnside.ConcreteSource.matrix_nil_kernel line 699
  88. theorem OAI.SourceBurnside.ConcreteSource.matrix_periodic line 701
  89. theorem OAI.SourceBurnside.ConcreteSource.image_element_periodic line 704
  90. def OAI.SourceBurnside.WordAlgebra.Table.gradingWords line 714
  91. def OAI.SourceBurnside.WordAlgebra.Table.gradingHom line 719
  92. lemma OAI.SourceBurnside.WordAlgebra.Table.gradingHom_word line 736
  93. lemma OAI.SourceBurnside.WordAlgebra.Table.algHom_ext_word line 740
  94. def OAI.SourceBurnside.WordAlgebra.Table.evalZero line 752
  95. def OAI.SourceBurnside.WordAlgebra.Table.evalOne line 754
  96. lemma OAI.SourceBurnside.WordAlgebra.Table.evalOne_gradingHom line 756
  97. lemma OAI.SourceBurnside.WordAlgebra.Table.evalZero_gradingHom line 761