OAI/GroupTheory/Congruence/Basic.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Polynomial congruence groups, truncation ideals, and finite nilpotent quotients.

  1. abbrev OAI.CoboundaryExpanders.Construction.R line 16
  2. def OAI.CoboundaryExpanders.Construction.powerIdeal line 17
  3. def OAI.CoboundaryExpanders.Construction.Gamma line 18
  4. abbrev OAI.CoboundaryExpanders.Construction.Trunc line 20
  5. instance OAI.CoboundaryExpanders.Construction.finiteTrunc line 22
  6. def OAI.CoboundaryExpanders.Construction.tbar line 27
  7. theorem OAI.CoboundaryExpanders.Construction.tbar_pow line 29
  8. theorem OAI.CoboundaryExpanders.Construction.exists_prime_power_unipotent line 33
  9. theorem OAI.CoboundaryExpanders.Construction.matrix_nilpotent_of_entries line 42
  10. theorem OAI.CoboundaryExpanders.Construction.strict_upper_pow_zero line 53
  11. theorem OAI.CoboundaryExpanders.Construction.prime_cast_trunc line 75
  12. theorem OAI.CoboundaryExpanders.Construction.mem_gamma_iff line 79
  13. theorem OAI.CoboundaryExpanders.Construction.gamma_antitone line 105
  14. theorem OAI.CoboundaryExpanders.Construction.reduction_sub_one_nilpotent line 111
  15. theorem OAI.CoboundaryExpanders.Construction.reduction_prime_power line 127
  16. def OAI.CoboundaryExpanders.Construction.congruenceReduction line 143
  17. def OAI.CoboundaryExpanders.Construction.deeperCongruence line 148
  18. theorem OAI.CoboundaryExpanders.Construction.deeperCongruence_eq line 151
  19. instance OAI.CoboundaryExpanders.Construction.normalDeeper line 154
  20. instance OAI.CoboundaryExpanders.Construction.finiteCongruenceQuotient line 157
  21. theorem OAI.CoboundaryExpanders.Construction.isPGroup_congruenceRange line 163
  22. theorem OAI.CoboundaryExpanders.Construction.isPGroup_congruenceQuotient line 175
  23. theorem OAI.CoboundaryExpanders.Construction.odd_congruence_index line 181
  24. def OAI.CoboundaryExpanders.Construction.IsUpperUnitriangular line 189
  25. def OAI.CoboundaryExpanders.Construction.upperUnitriangularMonoid line 194
  26. def OAI.CoboundaryExpanders.Construction.upperUnitriangular line 225
  27. def OAI.CoboundaryExpanders.Construction.evalZero line 235
  28. def OAI.CoboundaryExpanders.Construction.U line 239
  29. theorem OAI.CoboundaryExpanders.Construction.gamma_one_eq_ker_evalZero line 242
  30. theorem OAI.CoboundaryExpanders.Construction.gamma_le_U line 250
  31. theorem OAI.CoboundaryExpanders.Construction.upperUnitriangular_isPGroup line 258
  32. def OAI.CoboundaryExpanders.Construction.uReduction line 273
  33. def OAI.CoboundaryExpanders.Construction.Gquot line 277
  34. instance OAI.CoboundaryExpanders.Construction.(instance at line 278) line 278
  35. instance OAI.CoboundaryExpanders.Construction.(instance at line 279) line 279
  36. theorem OAI.CoboundaryExpanders.Construction.gquot_isPGroup line 283
  37. theorem OAI.CoboundaryExpanders.Construction.odd_gquot_card line 303
  38. abbrev OAI.CoboundaryExpanders.Construction.Frac line 311
  39. def OAI.CoboundaryExpanders.Construction.diagonalUnits line 313
  40. theorem OAI.CoboundaryExpanders.Construction.diagonalUnits_val line 320
  41. theorem OAI.CoboundaryExpanders.Construction.diagonalUnits_inv_val line 324
  42. def OAI.CoboundaryExpanders.Construction.cutUnit line 328
  43. def OAI.CoboundaryExpanders.Construction.edgeSource line 334
  44. theorem OAI.CoboundaryExpanders.Construction.edgeSource_ne line 337
  45. def OAI.CoboundaryExpanders.Construction.cycleRoot line 351
  46. def OAI.CoboundaryExpanders.Construction.localGroup line 356
  47. def OAI.CoboundaryExpanders.Construction.cutConjugation line 360
  48. theorem OAI.CoboundaryExpanders.Construction.cutConjugation_injective line 366
  49. theorem OAI.CoboundaryExpanders.Construction.diagonal_conj_transvection line 372
  50. theorem OAI.CoboundaryExpanders.Construction.cut_root_coefficient line 388
  51. theorem OAI.CoboundaryExpanders.Construction.map_transvection line 407
  52. theorem OAI.CoboundaryExpanders.Construction.cutConjugation_root line 416
  53. theorem OAI.CoboundaryExpanders.Construction.localGroup_le_constant line 430
  54. def OAI.CoboundaryExpanders.Construction.localGroupEmbedding line 440
  55. instance OAI.CoboundaryExpanders.Construction.localGroup_finite line 449
  56. theorem OAI.CoboundaryExpanders.Construction.localGroup_card_le line 458
  57. theorem OAI.CoboundaryExpanders.Construction.upper_transvection_mem_U line 467
  58. theorem OAI.CoboundaryExpanders.Construction.cycleRoot_mem_U line 481
  59. theorem OAI.CoboundaryExpanders.Construction.localGroup_le_U line 496
  60. def OAI.CoboundaryExpanders.Construction.uLocalGroup line 502
  61. def OAI.CoboundaryExpanders.Construction.uLocalEmbedding line 505
  62. instance OAI.CoboundaryExpanders.Construction.uLocalGroup_finite line 514
  63. def OAI.CoboundaryExpanders.Construction.reducedLocalGroup line 518
  64. def OAI.CoboundaryExpanders.Construction.reducedLocalMap line 522
  65. theorem OAI.CoboundaryExpanders.Construction.reducedLocalMap_surjective line 526
  66. theorem OAI.CoboundaryExpanders.Construction.reducedLocalGroup_card_le line 532
  67. theorem OAI.CoboundaryExpanders.Construction.card_trunc line 539
  68. def OAI.CoboundaryExpanders.Construction.reducedRoot line 548
  69. theorem OAI.CoboundaryExpanders.Construction.reducedRoot_injective line 557
  70. theorem OAI.CoboundaryExpanders.Construction.gquot_card_lower line 564
  71. def OAI.CoboundaryExpanders.Construction.cutPolynomial line 576
  72. theorem OAI.CoboundaryExpanders.Construction.cutUnit_coe line 579
  73. theorem OAI.CoboundaryExpanders.Construction.cutConjugation_apply line 584
  74. theorem OAI.CoboundaryExpanders.Construction.localGroup_entry_equation line 594
  75. theorem OAI.CoboundaryExpanders.Construction.localGroup_entry_degree_le_one line 608
  76. theorem OAI.CoboundaryExpanders.Construction.eq_of_small_degree_congruent line 626
  77. theorem OAI.CoboundaryExpanders.Construction.localGroups_reduction_injective line 639
  78. def OAI.CoboundaryExpanders.Construction.localQuotientMap line 651
  79. theorem OAI.CoboundaryExpanders.Construction.localQuotientMap_injective line 656
  80. theorem OAI.CoboundaryExpanders.Construction.localGroup_isPGroup line 664
  81. theorem OAI.CoboundaryExpanders.Construction.localGroup_odd line 669
  82. theorem OAI.CoboundaryExpanders.Construction.reducedLocalGroup_intersection line 675