OAI/Combinatorics/Progressions/Nilpotent/FactorwiseBCHCovers.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.piBCHSubgroup line 15
  2. theorem OAI.Erdos3.mem_piBCHSubgroup line 19
  3. theorem OAI.Erdos3.pi_basis_equivFun_symm_apply line 27
  4. theorem OAI.Erdos3.piBCHSubgroup_coordinates line 35
  5. theorem OAI.Erdos3.piBCHSubgroup_inner_grid line 45
  6. theorem OAI.Erdos3.piBCHSubgroup_outer_grid line 54
  7. def OAI.Erdos3.liePiSingle line 76
  8. def OAI.Erdos3.bchPiEquiv line 86
  9. def OAI.Erdos3.bchPiSingle line 97
  10. theorem OAI.Erdos3.bchPiEquiv_single line 102
  11. theorem OAI.Erdos3.bchPiSingle_eq_symm_mulSingle line 112
  12. theorem OAI.Erdos3.piBCHSubgroup_le_of_factors line 118
  13. theorem OAI.Erdos3.bchPiSingle_comap_inner_grid line 146
  14. theorem OAI.Erdos3.exists_factorwise_bch_covers line 166