OAI/Combinatorics/Progressions/Linear/RationalTaggedSpanProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalMatrix_real_ker_eq_range line 15
  2. theorem OAI.Erdos3.rationalMatrix_real_ker_eq_span line 46
  3. theorem OAI.Erdos3.matrixDenominator_le_exp_power line 64
  4. theorem OAI.Erdos3.matrix_weighted_factor_le_exp_power line 77
  5. theorem OAI.Erdos3.matrix_pair_denominator_le_exp_power line 102
  6. theorem OAI.Erdos3.rationalKernelSeparationConstant_ceil_le_exp_power line 141
  7. theorem OAI.Erdos3.real_basis_coordinates_transfer line 205
  8. theorem OAI.Erdos3.real_basis_coordinates_bound line 219
  9. theorem OAI.Erdos3.real_basis_coordinates_grid line 234
  10. theorem OAI.Erdos3.real_basis_transfer_denominator line 241
  11. theorem OAI.Erdos3.real_basis_coordinates_exp_bound line 252
  12. theorem OAI.Erdos3.exists_rationalTaggedSpanProjection line 275