OAI/GroupTheory/FiniteType/NonunitalCompression.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalCompression.unitValue line 13
  2. lemma OAI.NonunitalCompression.unitValue_one line 15
  3. lemma OAI.NonunitalCompression.unitValue_mul line 17
  4. def OAI.NonunitalCompression.units line 24
  5. lemma OAI.NonunitalCompression.units_val line 33
  6. def OAI.Steinberg.matrixCoefficient line 41
  7. lemma OAI.Steinberg.matrixCoefficient_apply line 48
  8. lemma OAI.Steinberg.matrix_map line 51
  9. lemma OAI.Steinberg.matrix_map_val line 65
  10. lemma OAI.Steinberg.map_preserves_kernel line 70
  11. def OAI.Steinberg.columnRoot line 82
  12. lemma OAI.Steinberg.columnRoot_commute line 86
  13. def OAI.Steinberg.column line 90
  14. lemma OAI.Steinberg.column_single line 108
  15. lemma OAI.Steinberg.root_conjugate_columnRoot line 126
  16. def OAI.Steinberg.matrixVector line 136
  17. lemma OAI.Steinberg.matrixVector_apply line 146
  18. lemma OAI.Steinberg.matrixVector_one line 149
  19. lemma OAI.Steinberg.matrixVector_mul line 154
  20. lemma OAI.Steinberg.matrixVector_root_single line 159
  21. lemma OAI.Steinberg.root_conjugate_column line 170
  22. lemma OAI.Steinberg.conjugate_column line 193
  23. lemma OAI.Steinberg.kernel_commute_column line 233
  24. lemma OAI.Steinberg.kernel_commute_outside_root line 245
  25. def OAI.Steinberg.rowRoot line 251
  26. lemma OAI.Steinberg.rowRoot_commute line 255
  27. def OAI.Steinberg.row line 259
  28. lemma OAI.Steinberg.row_single line 277
  29. lemma OAI.Steinberg.root_conjugate_rowRoot line 295
  30. def OAI.Steinberg.vectorMatrix line 306
  31. lemma OAI.Steinberg.vectorMatrix_apply line 316
  32. lemma OAI.Steinberg.vectorMatrix_one line 319
  33. lemma OAI.Steinberg.vectorMatrix_mul line 324
  34. lemma OAI.Steinberg.vectorMatrix_root_single line 329
  35. lemma OAI.Steinberg.root_conjugate_row line 341
  36. lemma OAI.Steinberg.conjugate_row line 364
  37. lemma OAI.Steinberg.kernel_commute_row line 404
  38. lemma OAI.Steinberg.kernel_commute_outside_row_root line 416
  39. lemma OAI.Steinberg.reindex_kernel_central line 422
  40. def OAI.Steinberg.matrixBlock line 452
  41. lemma OAI.Steinberg.matrixBlock_root line 467
  42. lemma OAI.Steinberg.matrix_reindex_inl line 476
  43. lemma OAI.Steinberg.pi_reindex_inl_one_iff line 486
  44. lemma OAI.Steinberg.block_kernel_central line 505
  45. lemma OAI.Steinberg.reindex_id line 514
  46. lemma OAI.Steinberg.reindex_trans line 523
  47. def OAI.Steinberg.matrixRelabel line 534
  48. lemma OAI.Steinberg.matrixRelabel_apply line 537
  49. lemma OAI.Steinberg.matrixRelabel_root line 540
  50. lemma OAI.Steinberg.matrix_reindex_equiv line 549
  51. def OAI.Steinberg.embeddingCompletion line 559
  52. lemma OAI.Steinberg.embeddingCompletion_inl line 565
  53. lemma OAI.Steinberg.matrix_reindex_entry line 568
  54. lemma OAI.Steinberg.kernel_of_reindex line 581
  55. def OAI.Steinberg.supported line 592
  56. lemma OAI.Steinberg.root_mem_supported line 596
  57. lemma OAI.Steinberg.supported_kernel_central line 602
  58. lemma OAI.Steinberg.column_mem_supported line 612
  59. lemma OAI.Steinberg.row_mem_supported line 625
  60. lemma OAI.Steinberg.matrixVector_single_apply line 637
  61. lemma OAI.Steinberg.vectorMatrix_single_apply line 642
  62. lemma OAI.Steinberg.conjugate_column_root_mem_supported line 648
  63. lemma OAI.Steinberg.conjugate_row_root_mem_supported line 662
  64. lemma OAI.Steinberg.reindex_commute_disjoint line 676
  65. lemma OAI.Steinberg.conjugate_coefficient_supported line 686
  66. lemma OAI.Steinberg.localized_coefficient_kernel_central line 733