OAI/Combinatorics/Progressions/Linear/AllocatedModularRankActualRefreshBad.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.extend_restrict_disjoint_fiber line 9
  2. theorem OAI.Erdos3.map_extend_selected line 33
  3. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceCoefficientReindex line 52
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_component line 61
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_component_reduce line 82
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_original_congruence line 102
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_rank_polynomial line 212
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_rank_probability line 229
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_modulusBad line 245
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_rankBad line 258
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedActualRefresh_badDepth line 274