OAI/Combinatorics/Progressions/Lattices/AllocatedModularRankIntegerDecay.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial line 18
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_degree line 40
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_top_reduce line 64
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_top_eq_actual_rank line 107
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_spatial_eval line 132
  6. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerSelectedCoefficients line 173
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerSelectedCoefficients_reduce line 186
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_rank_probability line 194
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerPolynomial_rank_of_good line 210
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_crt_characteristic_decay line 230
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_largest_bad_depth_good line 260
  12. def OAI.Erdos3.VectorPolynomial.allocatedCongruenceBadDepth line 270
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruence_crt_decay_of_bad_product line 275