OAI/Combinatorics/Progressions/Lattices/ScaledLatticeCovolume.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rational_vector_mem_span_integer_points line 15
  2. theorem OAI.Erdos3.exists_rational_matrix_height line 34
  3. theorem OAI.Erdos3.real_rational_kernel_eq_span_integer line 45
  4. theorem OAI.Erdos3.kernel_eq_span_integer_inter_of_basis line 101
  5. def OAI.Erdos3.latticeKernel line 162
  6. instance OAI.Erdos3.latticeKernel_discrete line 165
  7. theorem OAI.Erdos3.kernel_eq_span_lattice_inter line 168
  8. theorem OAI.Erdos3.latticeKernel_full line 177
  9. def OAI.Erdos3.latticeImageProjection line 202
  10. theorem OAI.Erdos3.latticeImageProjection_apply line 206
  11. theorem OAI.Erdos3.latticeImageProjection_surjective line 209
  12. def OAI.Erdos3.latticeKernelEquiv line 213
  13. theorem OAI.Erdos3.latticeKernelEquiv_apply line 223
  14. theorem OAI.Erdos3.exists_lattice_split_basis line 236
  15. theorem OAI.Erdos3.exists_lattice_basis_covolume_factor line 263
  16. theorem OAI.Erdos3.exists_lattice_index_covolume_factor line 313
  17. theorem OAI.Erdos3.exists_lattice_covolume_identity line 373
  18. theorem OAI.Erdos3.exists_scaled_lattice_covolume_identity line 405