OAI/GroupTheory/PeriodicGroups/Steinberg/KernelRelations.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Kernel.rootHom line 15
  2. abbrev OAI.SourceBurnside.Kernel.RectIndex line 20
  3. def OAI.SourceBurnside.Kernel.rectPosition line 24
  4. lemma OAI.SourceBurnside.Kernel.rect_commute line 27
  5. def OAI.SourceBurnside.Kernel.rectRoot line 38
  6. lemma OAI.SourceBurnside.Kernel.rectRoot_single line 42
  7. def OAI.SourceBurnside.Kernel.rectMatrix line 47
  8. lemma OAI.SourceBurnside.Kernel.rectMatrix_entry line 51
  9. lemma OAI.SourceBurnside.Kernel.rectMatrix_one line 55
  10. lemma OAI.SourceBurnside.Kernel.rectMatrix_mul line 59
  11. lemma OAI.SourceBurnside.Kernel.rectMatrix_product line 66
  12. def OAI.SourceBurnside.Kernel.rectUnits line 77
  13. lemma OAI.SourceBurnside.Kernel.coe_rectUnits line 92
  14. lemma OAI.SourceBurnside.Kernel.rectMatrix_single line 95
  15. lemma OAI.SourceBurnside.Kernel.rectUnits_single line 115
  16. lemma OAI.SourceBurnside.Kernel.representation_rectRoot line 122
  17. lemma OAI.SourceBurnside.Kernel.rectUnits_injective line 133
  18. def OAI.SourceBurnside.Kernel.Strip line 141
  19. lemma OAI.SourceBurnside.Kernel.strip_le_range line 145
  20. theorem OAI.SourceBurnside.Kernel.strip_faithful line 150
  21. def OAI.SourceBurnside.Root.map line 165
  22. def OAI.SourceBurnside.Steinberg.coordinateMap line 172
  23. theorem OAI.SourceBurnside.Steinberg.coordinateMap_x line 181
  24. lemma OAI.SourceBurnside.Steinberg.conjugate_chain line 185
  25. lemma OAI.SourceBurnside.Steinberg.conjugate_reverse line 194
  26. lemma OAI.SourceBurnside.Steinberg.conjugate_commute line 203
  27. lemma OAI.SourceBurnside.Steinberg.outside line 207
  28. theorem OAI.SourceBurnside.Steinberg.commutator_eq_top line 214
  29. theorem OAI.SourceBurnside.Steinberg.hom_to_commGroup_trivial line 227
  30. theorem OAI.SourceBurnside.Kernel.rational_detection line 243
  31. theorem OAI.SourceBurnside.Steinberg.periodic_of_finite_central_image line 266
  32. def OAI.SourceBurnside.Kernel.awayCoordinates line 287
  33. lemma OAI.SourceBurnside.Kernel.away_disjoint line 288
  34. def OAI.SourceBurnside.Kernel.columnStrip line 290
  35. def OAI.SourceBurnside.Kernel.rowStrip line 291
  36. lemma OAI.SourceBurnside.Kernel.column_root_mem line 292
  37. lemma OAI.SourceBurnside.Kernel.row_root_mem line 296
  38. lemma OAI.SourceBurnside.Kernel.conjugate_column_root_mem line 300
  39. lemma OAI.SourceBurnside.Kernel.conjugate_row_root_mem line 310
  40. lemma OAI.SourceBurnside.Kernel.conjugate_column_mem line 320
  41. lemma OAI.SourceBurnside.Kernel.conjugate_row_mem line 331
  42. def OAI.SourceBurnside.Kernel.away line 343
  43. lemma OAI.SourceBurnside.Kernel.away_le_column_normalizer line 345
  44. lemma OAI.SourceBurnside.Kernel.away_le_row_normalizer line 356
  45. lemma OAI.SourceBurnside.Kernel.kernel_commutes_column line 367
  46. lemma OAI.SourceBurnside.Kernel.kernel_commutes_row line 376
  47. theorem OAI.SourceBurnside.Kernel.supported_kernel_central line 386
  48. def OAI.SourceBurnside.Kernel.coordinateEquiv line 420
  49. def OAI.SourceBurnside.Kernel.coordinateIndex line 421
  50. lemma OAI.SourceBurnside.Kernel.coordinateIndex_injective line 422
  51. def OAI.SourceBurnside.Kernel.spareCoordinate line 424
  52. lemma OAI.SourceBurnside.Kernel.coordinateIndex_ne_spare line 425
  53. def OAI.SourceBurnside.Kernel.blockUnits line 430
  54. def OAI.SourceBurnside.Kernel.blockUnitsHom line 436
  55. def OAI.SourceBurnside.Kernel.padUnitsHom line 440
  56. lemma OAI.SourceBurnside.Kernel.padUnitsHom_e line 442
  57. def OAI.SourceBurnside.Kernel.padSteinberg line 455
  58. lemma OAI.SourceBurnside.Kernel.pad_representation line 457
  59. lemma OAI.SourceBurnside.Kernel.pad_mem_away line 463
  60. theorem OAI.SourceBurnside.Kernel.stabilized_kernel_central line 473
  61. lemma OAI.SourceBurnside.Steinberg.finite_central_image_periodic line 485
  62. lemma OAI.SourceBurnside.Kernel.padUnitsHom_injective line 522
  63. lemma OAI.SourceBurnside.Kernel.pad_kernel_iff line 532
  64. theorem OAI.SourceBurnside.Kernel.stabilized_field_periodic line 539
  65. lemma OAI.SourceBurnside.Elementary.map_e line 549
  66. lemma OAI.SourceBurnside.Elementary.representation_map line 557
  67. lemma OAI.SourceBurnside.Elementary.map_kernel line 563
  68. lemma OAI.SourceBurnside.Steinberg.map_comp line 570
  69. lemma OAI.SourceBurnside.Steinberg.map_map line 575
  70. lemma OAI.SourceBurnside.Steinberg.map_identity line 577
  71. lemma OAI.SourceBurnside.Steinberg.map_identity_apply line 581