OAI/Combinatorics/Progressions/Lattices/AllocatedModularRankAffineFullWitness.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerSelectedCoefficients_read line 14
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCongruenceIntegerSelectedCoefficients_refresh line 26
  3. def OAI.Erdos3.VectorPolynomial.allocatedResidueModulusBad line 58
  4. def OAI.Erdos3.VectorPolynomial.allocatedActualModulusBad line 71
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedActualModulusBad_eq_residue line 83
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedActualModulusBad_congr_residue line 97
  7. def OAI.Erdos3.VectorPolynomial.allocatedResiduePrimePowerWitness line 109
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedResiduePrimePowerWitness_iff_actual line 117
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalCongruenceTop_congr_outputs line 138
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueModulusBad_congr_outputs line 158
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedResiduePrimePowerWitness_congr_outputs line 169
  12. def OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad line 213
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_iff_modulusBad line 218
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_eq_rankBad line 228
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_false_of_notMem line 237
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_depth line 243
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_prescribedDeep_eq line 254
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_deep_depth line 264
  19. theorem OAI.Erdos3.VectorPolynomial.affineWitness_uniform_le line 291
  20. def OAI.Erdos3.VectorPolynomial.allocatedAffineMixedModulusBad line 323
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineMixedModulusBad_probability line 332
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineMixed_primePower_event line 355
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineMixedActual_primePower_event line 391
  24. theorem OAI.Erdos3.VectorPolynomial.affine_decide_eq_classical line 433
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineProductMixed_primePower_event line 460