OAI/Combinatorics/Progressions/Lattices/IntegerColumnMinor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integer_det_natAbs_le line 16
  2. theorem OAI.Erdos3.integer_cramer_natAbs_le line 27
  3. def OAI.Erdos3.rationalCramerSolution line 38
  4. theorem OAI.Erdos3.rationalCramerSolution_solves line 41
  5. theorem OAI.Erdos3.rationalCramerSolution_unique line 46
  6. theorem OAI.Erdos3.integerCramerSolution_apply line 52
  7. theorem OAI.Erdos3.integerCramerSolution_height line 67
  8. theorem OAI.Erdos3.exists_bounded_integer_system_solution line 77
  9. theorem OAI.Erdos3.integerColumnMinor_range_le line 98
  10. theorem OAI.Erdos3.integerColumnMinor_det_bound line 106
  11. theorem OAI.Erdos3.nonzeroMinor_largeCokernelEvent line 111