OAI/GroupTheory/Congruence/Elementary.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Elementary matrices, Euclidean generation, block matrices, and residue-field pivot arguments.

  1. abbrev OAI.CoboundaryExpanders.Elementary.E line 19
  2. theorem OAI.CoboundaryExpanders.Elementary.E_mul_apply line 22
  3. def OAI.CoboundaryExpanders.Elementary.Upper line 32
  4. theorem OAI.CoboundaryExpanders.Elementary.upper_E_mul line 35
  5. def OAI.CoboundaryExpanders.Elementary.Cleared line 46
  6. theorem OAI.CoboundaryExpanders.Elementary.clear_step line 49
  7. theorem OAI.CoboundaryExpanders.Elementary.upper_mem_of_transvections line 100
  8. theorem OAI.CoboundaryExpanders.Elementary.E_commutator line 127
  9. def OAI.CoboundaryExpanders.Blocks.reindexSL line 144
  10. theorem OAI.CoboundaryExpanders.Blocks.reindexSL_apply line 151
  11. theorem OAI.CoboundaryExpanders.Blocks.reindexSL_map line 156
  12. def OAI.CoboundaryExpanders.Blocks.blockSL line 160
  13. theorem OAI.CoboundaryExpanders.Blocks.blockSL_map line 171
  14. def OAI.CoboundaryExpanders.Blocks.stabilizeSL line 178
  15. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_map line 182
  16. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_right_row line 187
  17. theorem OAI.CoboundaryExpanders.Blocks.stabilizeSL_right_col line 197
  18. theorem OAI.CoboundaryExpanders.Elementary.E_path_mem line 212
  19. theorem OAI.CoboundaryExpanders.Elementary.E_natCast_mul line 218
  20. theorem OAI.CoboundaryExpanders.Elementary.E_upper_one_mem line 229
  21. theorem OAI.CoboundaryExpanders.Elementary.clear_step_relative line 244
  22. theorem OAI.CoboundaryExpanders.Elementary.upper_subgroup_le line 295
  23. def OAI.CoboundaryExpanders.Elementary.OffCleared line 337
  24. theorem OAI.CoboundaryExpanders.Elementary.off_clear_step line 340
  25. theorem OAI.CoboundaryExpanders.Elementary.diagonalize_iwahori line 414
  26. def OAI.CoboundaryExpanders.Elementary.D line 438
  27. theorem OAI.CoboundaryExpanders.Elementary.D_mul_apply line 443
  28. theorem OAI.CoboundaryExpanders.Elementary.D_mem line 460
  29. theorem OAI.CoboundaryExpanders.Elementary.diagonal_iwahori_mem line 472
  30. theorem OAI.CoboundaryExpanders.Elementary.iwahori_mem_of_roots line 545
  31. def OAI.CoboundaryExpanders.Elementary.ColumnPrefix line 572
  32. theorem OAI.CoboundaryExpanders.Elementary.inverse_column_sum line 575
  33. theorem OAI.CoboundaryExpanders.Elementary.column_diagonal_unit line 581
  34. theorem OAI.CoboundaryExpanders.Elementary.inverse_prefix_zero line 589
  35. theorem OAI.CoboundaryExpanders.Elementary.columnPrefix_E_mul line 599
  36. def OAI.CoboundaryExpanders.Elementary.W line 606
  37. theorem OAI.CoboundaryExpanders.Elementary.W_mul_apply line 609
  38. theorem OAI.CoboundaryExpanders.Elementary.W_mem line 619
  39. theorem OAI.CoboundaryExpanders.Elementary.columnPrefix_W_mul line 623
  40. theorem OAI.CoboundaryExpanders.Elementary.lower_column_nonzero line 636
  41. theorem OAI.CoboundaryExpanders.Elementary.exists_unit_pivot line 652
  42. theorem OAI.CoboundaryExpanders.Elementary.clear_column line 716
  43. theorem OAI.CoboundaryExpanders.Elementary.diagonalize_polynomial line 762
  44. theorem OAI.CoboundaryExpanders.Elementary.diagonal_mem_of_roots line 786
  45. theorem OAI.CoboundaryExpanders.Elementary.polynomial_SL_mem_of_roots line 858
  46. theorem OAI.CoboundaryExpanders.Elementary.mul_E_apply line 875
  47. theorem OAI.CoboundaryExpanders.Elementary.elementary_commutes_of_complement line 884
  48. theorem OAI.CoboundaryExpanders.Elementary.restricted_euclidean_descent line 916
  49. theorem OAI.CoboundaryExpanders.Elementary.exists_unit_pivot_iwahori line 968
  50. theorem OAI.CoboundaryExpanders.Elementary.clear_column_iwahori line 1018
  51. theorem OAI.CoboundaryExpanders.Elementary.diagonalize_polynomial_iwahori line 1068
  52. theorem OAI.CoboundaryExpanders.Elementary.polynomial_iwahori_mem_of_roots line 1091
  53. lemma OAI.CoboundaryExpanders.Elementary.exists_unit_pivot_residue line 1122
  54. lemma OAI.CoboundaryExpanders.Elementary.diagonalize_residue line 1151
  55. theorem OAI.CoboundaryExpanders.Elementary.SL_mem_of_residue_units line 1170
  56. theorem OAI.CoboundaryExpanders.Elementary.SL_map_surjective line 1183
  57. lemma OAI.CoboundaryExpanders.Elementary.SL_map_surjective_reindex line 1207