OAI/Combinatorics/Progressions/Lattices/CoverBasisResidues.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.coverLatticePoint line 13
  2. theorem OAI.Erdos3.coverLatticePoint_val line 22
  3. theorem OAI.Erdos3.coverLatticePoint_surjective line 26
  4. theorem OAI.Erdos3.coverLatticePoint_ker line 41
  5. abbrev OAI.Erdos3.CoverLatticeResidue line 63
  6. def OAI.Erdos3.coverLatticeResidueEquiv line 65
  7. theorem OAI.Erdos3.coverLatticeResidueEquiv_mk line 71
  8. def OAI.Erdos3.latticeBasisResidue line 88
  9. theorem OAI.Erdos3.latticeBasisResidue_surjective line 92
  10. theorem OAI.Erdos3.latticeBasisResidue_ker line 97
  11. def OAI.Erdos3.coverLatticeBasisEquiv line 119
  12. theorem OAI.Erdos3.coverLatticeBasisEquiv_mk line 126
  13. def OAI.Erdos3.coverKernelBasisEquiv line 130
  14. theorem OAI.Erdos3.coverKernelBasisEquiv_residue line 134
  15. theorem OAI.Erdos3.coverKernel_card line 142