OAI/Combinatorics/Progressions/Lattices/IntegerFrozenChart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.frozenCoordinate line 13
  2. def OAI.Erdos3.freezePolynomial line 17
  3. theorem OAI.Erdos3.frozenCoordinate_support line 21
  4. theorem OAI.Erdos3.freezePolynomial_support line 29
  5. theorem OAI.Erdos3.freezePolynomial_degree line 34
  6. theorem OAI.Erdos3.freezePolynomial_eval line 40
  7. theorem OAI.Erdos3.freezePolynomial_sub_lower line 51
  8. theorem OAI.Erdos3.freezePolynomial_top_independent line 68
  9. theorem OAI.Erdos3.freezePolynomial_map line 87
  10. theorem OAI.Erdos3.frozenCoordinate_zero_homogeneous line 98
  11. theorem OAI.Erdos3.freezePolynomial_top line 107