OAI/Combinatorics/Progressions/Estimates/PowerSubgroup.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.powerSubgroup line 13
  2. theorem OAI.Erdos3.pow_mem_powerSubgroup line 16
  3. theorem OAI.Erdos3.powerSubgroup_map_le line 19
  4. instance OAI.Erdos3.powerSubgroup_characteristic line 28
  5. def OAI.Erdos3.subgroupPowerCover line 31
  6. theorem OAI.Erdos3.subgroupPowerCover_le line 34
  7. theorem OAI.Erdos3.pow_mem_subgroupPowerCover line 38
  8. theorem OAI.Erdos3.subgroupPowerCover_le_iff line 42
  9. theorem OAI.Erdos3.subgroupPowerCover_subgroupOf line 53
  10. instance OAI.Erdos3.subgroupPowerCover_characteristic line 58
  11. instance OAI.Erdos3.subgroupPowerCover_normal line 63