OAI/Combinatorics/Progressions/Nilpotent/BCHSubgroupGridExistence.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieBCHGroup.quotientHom line 16
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientHom_coord line 21
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientHom_surjective line 24
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientHom_ker line 30
  5. def OAI.Erdos3.NilpotentLieBCHGroup.quotientEquiv line 42
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientEquiv_mk line 47
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.subgroup_ideal_normal line 50
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.commute_of_lie_eq_zero line 55
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.commutator_mem_ideal line 62
  10. theorem OAI.Erdos3.lieBCH_sub_add_mem line 89
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.additive_remainder_mem line 100
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_pow line 129
  13. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_zpow line 137
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_pow_rat line 146
  15. structure OAI.Erdos3.NilpotentLieFiltration line 159
  16. def OAI.Erdos3.NilpotentLieFiltration.layerIdeal line 170
  17. theorem OAI.Erdos3.NilpotentLieFiltration.mem_layerIdeal line 177
  18. theorem OAI.Erdos3.NilpotentLieFiltration.lowerCentralSeries_le line 179
  19. theorem OAI.Erdos3.NilpotentLieFiltration.lowerCentralSeries_eq_bot line 194
  20. abbrev OAI.Erdos3.NilpotentLieFiltration.Group line 202
  21. theorem OAI.Erdos3.NilpotentLieFiltration.bch_mem line 204
  22. def OAI.Erdos3.NilpotentLieFiltration.subgroup line 208
  23. theorem OAI.Erdos3.NilpotentLieFiltration.mem_subgroup line 211
  24. theorem OAI.Erdos3.NilpotentLieFiltration.subgroup_normal line 213
  25. theorem OAI.Erdos3.NilpotentLieFiltration.commutator_mem line 216
  26. theorem OAI.Erdos3.NilpotentLieFiltration.subgroup_one line 221
  27. theorem OAI.Erdos3.NilpotentLieFiltration.subgroup_terminal line 227
  28. theorem OAI.Erdos3.NilpotentLieFiltration.descendingCentralSeries line 236
  29. theorem OAI.Erdos3.NilpotentLieFiltration.group_lowerCentralSeries_eq_bot line 244
  30. theorem OAI.Erdos3.NilpotentLieFiltration.isNilpotentGroup line 249
  31. theorem OAI.Erdos3.NilpotentLieFiltration.nilpotencyClass_le line 252
  32. def OAI.Erdos3.bchSubgroupCoordinates line 273
  33. theorem OAI.Erdos3.bchSubgroupCoordinates_comap line 280
  34. theorem OAI.Erdos3.bchSubgroupCoordinates_map line 293
  35. theorem OAI.Erdos3.exists_bchSubgroup_comap_grid_exp_bound line 319
  36. theorem OAI.Erdos3.exists_bchSubgroup_map_grid_exp_bound line 336
  37. theorem OAI.Erdos3.NilpotentLieBCHGroup.descendingCentralSeries line 362
  38. theorem OAI.Erdos3.NilpotentLieBCHGroup.lowerCentralSeries_eq_bot line 378
  39. theorem OAI.Erdos3.NilpotentLieBCHGroup.isNilpotentGroup line 389
  40. theorem OAI.Erdos3.NilpotentLieBCHGroup.nilpotencyClass_le line 392
  41. def OAI.Erdos3.NilpotentLieBCHGroup.conjugationCoord line 407
  42. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationCoord_nsmul line 410
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationCoord_zsmul line 420
  44. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationCoord_rat_smul line 430
  45. theorem OAI.Erdos3.NilpotentLieFiltration.quotient_bch_eq_add line 459
  46. theorem OAI.Erdos3.NilpotentLieFiltration.quotient_prod_eq_sum line 469
  47. theorem OAI.Erdos3.NilpotentLieFiltration.exists_product_of_layerwise_sum line 488
  48. theorem OAI.Erdos3.NilpotentLieFiltration.exists_product_of_layerwise_range line 528
  49. theorem OAI.Erdos3.exists_bchSubgroup_comap_grid line 557