OAI/GroupTheory/Congruence/Patterns.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

Pattern subgroups, matrix opposition, block decompositions, and suffix equivalences.

  1. def OAI.CoboundaryExpanders.Patterns.cutRank line 22
  2. theorem OAI.CoboundaryExpanders.Patterns.cutRank_injective line 26
  3. def OAI.CoboundaryExpanders.Patterns.cutOrder line 33
  4. def OAI.CoboundaryExpanders.Patterns.Arc line 36
  5. theorem OAI.CoboundaryExpanders.Patterns.cutRank_lt_iff line 40
  6. def OAI.CoboundaryExpanders.Patterns.reindexSL line 48
  7. theorem OAI.CoboundaryExpanders.Patterns.reindexSL_apply line 59
  8. theorem OAI.CoboundaryExpanders.Patterns.reindexSL_E line 65
  9. def OAI.CoboundaryExpanders.Patterns.upperMonoid line 76
  10. theorem OAI.CoboundaryExpanders.Patterns.upper_prime_power line 100
  11. def OAI.CoboundaryExpanders.Patterns.upperSubgroup line 114
  12. def OAI.CoboundaryExpanders.Patterns.cutUpper line 126
  13. theorem OAI.CoboundaryExpanders.Patterns.cutUpper_iff line 129
  14. theorem OAI.CoboundaryExpanders.Patterns.localGroup_le_cutUpper line 142
  15. def OAI.CoboundaryExpanders.Patterns.rootGroup line 178
  16. def OAI.CoboundaryExpanders.Patterns.intersectionGroup line 182
  17. theorem OAI.CoboundaryExpanders.Patterns.mem_intersectionGroup line 187
  18. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_le_intersection line 193
  19. theorem OAI.CoboundaryExpanders.Patterns.root_mem line 203
  20. theorem OAI.CoboundaryExpanders.Patterns.upper_adjacent_mem line 207
  21. theorem OAI.CoboundaryExpanders.Patterns.upper_path_mem line 218
  22. theorem OAI.CoboundaryExpanders.Patterns.lower_path_mem line 236
  23. theorem OAI.CoboundaryExpanders.Patterns.scalar_root_mem line 263
  24. def OAI.CoboundaryExpanders.Patterns.pathCoefficient line 272
  25. theorem OAI.CoboundaryExpanders.Patterns.path_root_mem line 275
  26. theorem OAI.CoboundaryExpanders.Patterns.entry_nonzero_path line 293
  27. theorem OAI.CoboundaryExpanders.Patterns.intersection_diagonal line 306
  28. theorem OAI.CoboundaryExpanders.Patterns.local_entry_coefficient line 314
  29. theorem OAI.CoboundaryExpanders.Patterns.entry_root_mem line 340
  30. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_eq_intersection line 357
  31. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_inter line 385
  32. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_empty line 405
  33. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_compl_singleton line 409
  34. theorem OAI.CoboundaryExpanders.Patterns.iInf_localGroup_eq_bot line 413
  35. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_reduction_injective line 417
  36. theorem OAI.CoboundaryExpanders.Patterns.reduction_preserves_rootGroup_intersections line 427
  37. def OAI.CoboundaryExpanders.Patterns.standardLocalGroup line 446
  38. theorem OAI.CoboundaryExpanders.Patterns.rootGroup_image_eq_standard line 450
  39. def OAI.CoboundaryExpanders.Patterns.localStandardEquiv line 473
  40. abbrev OAI.CoboundaryExpanders.MatrixOpposition.stdFlag line 489
  41. abbrev OAI.CoboundaryExpanders.MatrixOpposition.oppFlag line 491
  42. lemma OAI.CoboundaryExpanders.MatrixOpposition.stdFlags_opposite line 494
  43. lemma OAI.CoboundaryExpanders.MatrixOpposition.upper_iff_unipotent line 497
  44. def OAI.CoboundaryExpanders.MatrixOpposition.upperGroup line 505
  45. lemma OAI.CoboundaryExpanders.MatrixOpposition.mem_upperGroup line 508
  46. def OAI.CoboundaryExpanders.MatrixOpposition.upperToFlag line 511
  47. lemma OAI.CoboundaryExpanders.MatrixOpposition.upperToFlag_injective line 516
  48. lemma OAI.CoboundaryExpanders.MatrixOpposition.upperToFlag_surjective line 521
  49. def OAI.CoboundaryExpanders.MatrixOpposition.upperFlagEquiv line 549
  50. lemma OAI.CoboundaryExpanders.MatrixOpposition.upper_E line 552
  51. lemma OAI.CoboundaryExpanders.MatrixOpposition.preserves_suffix_iff line 556
  52. def OAI.CoboundaryExpanders.MatrixOpposition.suffixStabilizer line 591
  53. def OAI.CoboundaryExpanders.MatrixOpposition.patternGroup line 596
  54. lemma OAI.CoboundaryExpanders.MatrixOpposition.mem_suffixStabilizer line 600
  55. lemma OAI.CoboundaryExpanders.MatrixOpposition.mem_patternGroup line 608
  56. def OAI.CoboundaryExpanders.MatrixOpposition.pathGroup line 622
  57. lemma OAI.CoboundaryExpanders.MatrixOpposition.adjacent_mem_pathGroup line 627
  58. lemma OAI.CoboundaryExpanders.MatrixOpposition.pathGroup_le_pattern line 632
  59. lemma OAI.CoboundaryExpanders.MatrixOpposition.E_path_one_mem line 649
  60. lemma OAI.CoboundaryExpanders.MatrixOpposition.E_path_mem_coeff line 668
  61. theorem OAI.CoboundaryExpanders.MatrixOpposition.pathGroup_eq_pattern line 676
  62. lemma OAI.CoboundaryExpanders.MatrixOpposition.full_pathGroup line 691
  63. lemma OAI.CoboundaryExpanders.MatrixOpposition.pathGroup_inter line 696
  64. lemma OAI.CoboundaryExpanders.MatrixOpposition.pathGroup_delete line 707
  65. lemma OAI.CoboundaryExpanders.Patterns.cutOrder_cut line 722
  66. lemma OAI.CoboundaryExpanders.Patterns.cutOrder_edgeSource line 727
  67. theorem OAI.CoboundaryExpanders.Patterns.standard_reindex_eq_path line 745
  68. lemma OAI.CoboundaryExpanders.Patterns.cutOrder_image_compl line 770
  69. lemma OAI.CoboundaryExpanders.Patterns.pathGroup_compl_zero line 785
  70. theorem OAI.CoboundaryExpanders.Patterns.standard_max_reindex line 791
  71. def OAI.CoboundaryExpanders.Patterns.standardMaxFlagEquiv line 796
  72. def OAI.CoboundaryExpanders.Patterns.localFlagEquiv line 803
  73. lemma OAI.CoboundaryExpanders.Patterns.localStandardEquiv_equation line 816
  74. lemma OAI.CoboundaryExpanders.Patterns.localStandardEquiv_mem_iff line 824
  75. lemma OAI.CoboundaryExpanders.Patterns.reindex_mem_iff line 852
  76. lemma OAI.CoboundaryExpanders.Patterns.two_cuts_image line 863
  77. lemma OAI.CoboundaryExpanders.Patterns.pathGroup_delete_zero line 870
  78. lemma OAI.CoboundaryExpanders.Patterns.standardMaxFlagEquiv_value line 875
  79. theorem OAI.CoboundaryExpanders.Patterns.standardMaxFlagEquiv_stabilizer line 880
  80. theorem OAI.CoboundaryExpanders.Patterns.localFlagEquiv_stabilizer line 894
  81. lemma OAI.CoboundaryExpanders.Patterns.cutOrder_pos line 915
  82. def OAI.CoboundaryExpanders.Patterns.localTypeIndex line 921
  83. lemma OAI.CoboundaryExpanders.Patterns.localTypeIndex_bijective line 924
  84. def OAI.CoboundaryExpanders.Patterns.localTypeEquiv line 952
  85. lemma OAI.CoboundaryExpanders.Patterns.localTypeEquiv_rank line 955
  86. def OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix line 970
  87. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_ll line 974
  88. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_rr line 979
  89. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_lr line 984
  90. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_rl line 989
  91. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_det line 995
  92. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_mul line 999
  93. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_one line 1008
  94. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockMatrix_upper line 1014
  95. def OAI.CoboundaryExpanders.MatrixOpposition.blockUpper line 1035
  96. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockUpper_injective line 1042
  97. lemma OAI.CoboundaryExpanders.MatrixOpposition.upper_submatrix line 1054
  98. theorem OAI.CoboundaryExpanders.MatrixOpposition.range_blockUpper line 1071
  99. def OAI.CoboundaryExpanders.MatrixOpposition.blockRangeEquiv line 1102
  100. def OAI.CoboundaryExpanders.MatrixOpposition.suffixGroup line 1111
  101. lemma OAI.CoboundaryExpanders.MatrixOpposition.mem_suffixGroup line 1116
  102. lemma OAI.CoboundaryExpanders.MatrixOpposition.range_blockUpper_eq_suffixGroup line 1123
  103. def OAI.CoboundaryExpanders.MatrixOpposition.blockSuffixEquiv line 1128
  104. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockSuffixEquiv_val line 1132
  105. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockUpper_suffix_left line 1135
  106. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockUpper_suffix_right line 1154
  107. abbrev OAI.CoboundaryExpanders.MatrixOpposition.Cut line 1173
  108. def OAI.CoboundaryExpanders.MatrixOpposition.cutGroups line 1174
  109. def OAI.CoboundaryExpanders.MatrixOpposition.cutSplitEquiv line 1177
  110. lemma OAI.CoboundaryExpanders.MatrixOpposition.blockSuffix_system line 1207