OAI/Combinatorics/Progressions/Polynomial/FrozenPolynomialAffineRange.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.freezePolynomial_monomial_eq_C_of_no_keep line 15
  2. theorem OAI.Erdos3.freezePolynomial_monomial_coeff_eq_zero_of_no_keep line 29
  3. theorem OAI.Erdos3.polynomialFamily_eval_mem line 47
  4. theorem OAI.Erdos3.longChart_top_eval_mem line 71
  5. theorem OAI.Erdos3.longChart_conditioned_top_eval_mem line 90
  6. theorem OAI.Erdos3.longChart_freezePolynomial_zero_eq_killCompl line 106
  7. theorem OAI.Erdos3.longChart_frozen_top_eval_mem line 125
  8. theorem OAI.Erdos3.polynomialFamily_freeze_coeff_mem line 155
  9. theorem OAI.Erdos3.sub_projected_anchor_mem line 205
  10. theorem OAI.Erdos3.polynomialFamily_eval_sub_zero_mem line 212
  11. theorem OAI.Erdos3.polynomialFamily_linearMap_eval_eq_zero line 226
  12. theorem OAI.Erdos3.polynomialFamily_quotient_eval_eq_zero line 236
  13. theorem OAI.Erdos3.frozenPolynomialFamily_coeff_mem line 243
  14. theorem OAI.Erdos3.frozenPolynomialFamily_eval_sub_zero_mem line 260
  15. theorem OAI.Erdos3.frozenPolynomialFamily_linearMap_eval_eq_zero line 273