OAI/GroupTheory/PeriodicGroups/Steinberg/BlockEmbeddings.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Kernel.blockIndex line 12
  2. lemma OAI.SourceBurnside.Kernel.blockIndex_ne line 13
  3. def OAI.SourceBurnside.Kernel.blockPosition line 16
  4. lemma OAI.SourceBurnside.Kernel.block_factors_commute line 18
  5. def OAI.SourceBurnside.Kernel.blockHom line 23
  6. def OAI.SourceBurnside.Kernel.blockRoot line 27
  7. lemma OAI.SourceBurnside.Kernel.blockRoot_zero line 29
  8. lemma OAI.SourceBurnside.Kernel.blockRoot_add line 31
  9. lemma OAI.SourceBurnside.Kernel.blockRoot_single line 34
  10. lemma OAI.SourceBurnside.Kernel.blockRoot_commute line 44
  11. lemma OAI.SourceBurnside.Kernel.blockRoot_mul line 55
  12. def OAI.SourceBurnside.Kernel.blockMap line 88
  13. lemma OAI.SourceBurnside.Kernel.blockMap_x line 92
  14. def OAI.SourceBurnside.Kernel.flattenRing line 101
  15. lemma OAI.SourceBurnside.Kernel.flatten_single line 103
  16. lemma OAI.SourceBurnside.Kernel.representation_blockRoot line 113
  17. lemma OAI.SourceBurnside.Kernel.block_representation line 124
  18. lemma OAI.SourceBurnside.Kernel.blockMap_kernel line 130
  19. def OAI.SourceBurnside.Kernel.rowFixed line 142
  20. lemma OAI.SourceBurnside.Kernel.root_rowFixed line 164
  21. lemma OAI.SourceBurnside.Kernel.strip_eq_one_of_rows line 168
  22. lemma OAI.SourceBurnside.Kernel.right_conjugate_strip_root line 182
  23. lemma OAI.SourceBurnside.Kernel.right_conjugate_strip line 197
  24. def OAI.SourceBurnside.Kernel.triangular line 207
  25. def OAI.SourceBurnside.Kernel.layer line 209
  26. def OAI.SourceBurnside.Kernel.above line 210
  27. lemma OAI.SourceBurnside.Kernel.layer_above_disjoint line 211
  28. lemma OAI.SourceBurnside.Kernel.deeper_normalizes_strip line 216
  29. lemma OAI.SourceBurnside.Kernel.deeper_fixes_layer line 230
  30. lemma OAI.SourceBurnside.Kernel.triangular_split line 239
  31. lemma OAI.SourceBurnside.Kernel.triangular_faithful_aux line 268
  32. theorem OAI.SourceBurnside.Kernel.triangular_faithful line 296
  33. lemma OAI.SourceBurnside.Kernel.level_conjugate_triangular_root line 300
  34. lemma OAI.SourceBurnside.Kernel.level_conjugate_triangular line 334
  35. theorem OAI.SourceBurnside.Kernel.level_root_normalizes line 344
  36. lemma OAI.SourceBurnside.Steinberg.hom_images_commute line 359
  37. lemma OAI.SourceBurnside.Kernel.blockIndex_ne_inner line 382
  38. def OAI.SourceBurnside.Kernel.copyMap line 385
  39. lemma OAI.SourceBurnside.Kernel.copyMap_x line 388
  40. lemma OAI.SourceBurnside.Kernel.copy_commute line 390
  41. def OAI.SourceBurnside.Kernel.copyFamily line 398
  42. def OAI.SourceBurnside.Kernel.diagonalCopy line 401
  43. def OAI.SourceBurnside.Kernel.diagonalBlockHom line 405
  44. def OAI.SourceBurnside.Kernel.copyRoots line 411
  45. lemma OAI.SourceBurnside.Kernel.diagonalBlockHom_eq line 414
  46. lemma OAI.SourceBurnside.Kernel.diagonalCopy_x line 424
  47. def OAI.SourceBurnside.Kernel.innerHeight line 428
  48. lemma OAI.SourceBurnside.Kernel.innerHeight_blockIndex line 429
  49. def OAI.SourceBurnside.Kernel.upper line 431
  50. lemma OAI.SourceBurnside.Kernel.upper_faithful line 432
  51. lemma OAI.SourceBurnside.Kernel.strict_block_mem_upper line 434
  52. lemma OAI.SourceBurnside.Kernel.diagonalCopy_normalizes line 447
  53. def OAI.SourceBurnside.Kernel.numericMatrix line 471
  54. lemma OAI.SourceBurnside.Kernel.numeric_scalar_commute line 473
  55. def OAI.SourceBurnside.Kernel.matrixEval line 480
  56. def OAI.SourceBurnside.Kernel.scalarEval line 482
  57. def OAI.SourceBurnside.Kernel.matrixEvalRingHom line 485
  58. def OAI.SourceBurnside.Kernel.matrixSteinbergEval line 494
  59. lemma OAI.SourceBurnside.Kernel.matrixSteinbergEval_kernel line 496
  60. lemma OAI.SourceBurnside.Kernel.scalarEval_kernel line 501
  61. lemma OAI.SourceBurnside.Kernel.numeric_upper line 504
  62. lemma OAI.SourceBurnside.Kernel.triangular_mul_diag line 510
  63. lemma OAI.SourceBurnside.Kernel.triangular_pow_diag line 520
  64. lemma OAI.SourceBurnside.Kernel.matrixEval_upper line 525
  65. lemma OAI.SourceBurnside.Kernel.matrixEval_diag line 533
  66. def OAI.SourceBurnside.Kernel.scalarRingHom line 552
  67. lemma OAI.SourceBurnside.Kernel.diagonalCopy_eq line 560
  68. lemma OAI.SourceBurnside.Kernel.diagonalCopy_kernel line 566
  69. lemma OAI.SourceBurnside.Kernel.triangular_entry_split line 572
  70. lemma OAI.SourceBurnside.Kernel.triangular_collect line 595
  71. theorem OAI.SourceBurnside.Kernel.triangular_evaluation line 630