OAI/Combinatorics/Progressions/Estimates/RationalRowReduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rationalSolveHeight line 14
  2. theorem OAI.Erdos3.exists_bounded_rational_system_solution line 19
  3. theorem OAI.Erdos3.rationalCramerSolution_height line 65
  4. theorem OAI.Erdos3.rationalHeightLE_zero line 74
  5. theorem OAI.Erdos3.rationalHeightLE_one line 77
  6. theorem OAI.Erdos3.exists_bounded_rational_right_inverse line 80
  7. theorem OAI.Erdos3.RationalHeightLE.neg line 107
  8. theorem OAI.Erdos3.RationalHeightLE.mul line 111
  9. theorem OAI.Erdos3.RationalHeightLE.add line 124
  10. theorem OAI.Erdos3.RationalHeightLE.sub line 152
  11. theorem OAI.Erdos3.rationalHeightLE_sum line 157
  12. theorem OAI.Erdos3.rationalHeightLE_matrix_mul line 178
  13. theorem OAI.Erdos3.exists_nonsingular_columns line 199
  14. def OAI.Erdos3.extendRows line 227
  15. theorem OAI.Erdos3.extendRows_apply line 231
  16. theorem OAI.Erdos3.extendRows_apply_of_not_mem line 237
  17. theorem OAI.Erdos3.mul_extendRows line 244
  18. theorem OAI.Erdos3.rationalSolveHeight_pos line 256
  19. theorem OAI.Erdos3.exists_bounded_rational_section line 262
  20. theorem OAI.Erdos3.rationalHeightLE_prod line 290
  21. theorem OAI.Erdos3.rational_product_exp_height line 305
  22. theorem OAI.Erdos3.rational_sum_cost_le_exp line 322
  23. theorem OAI.Erdos3.rational_sum_exp_height line 344
  24. theorem OAI.Erdos3.mulVec_eq_zero_iff_row_span line 373
  25. theorem OAI.Erdos3.mulVec_surjective_of_independent_rows line 388
  26. theorem OAI.Erdos3.exists_independent_defining_rows line 396