OAI/Combinatorics/Progressions/Sampling/GridNormalizationDenominator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_integer_scaled_grid_matrix line 11
  2. theorem OAI.Erdos3.scaled_integer_minor_eq line 19
  3. theorem OAI.Erdos3.scaled_integer_minor_natAbs_bound line 32
  4. theorem OAI.Erdos3.exists_bounded_rational_grid_matrix line 55
  5. theorem OAI.Erdos3.exists_bounded_rational_map_matrix line 88
  6. theorem OAI.Erdos3.scaled_integer_row_normalization_cast line 117
  7. theorem OAI.Erdos3.exists_bounded_rational_row_normalization line 135
  8. theorem OAI.Erdos3.integer_row_normalization_grid line 173
  9. theorem OAI.Erdos3.exists_grid_row_normalization line 196