OAI/Combinatorics/Progressions/Polynomial/RawCanonicalNormalizedPolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.rawProductArrayPolynomial line 11
  2. theorem OAI.Erdos3.rawProductArrayPolynomial_eval line 19
  3. theorem OAI.Erdos3.rawProductArrayJet_polynomial line 28
  4. theorem OAI.Erdos3.rawProductArrayPolynomial_totalDegree_le line 40
  5. theorem OAI.Erdos3.polynomial_coefficient_split line 75
  6. def OAI.Erdos3.nonprincipalSupport line 88
  7. theorem OAI.Erdos3.polynomial_coefficient_split_principal line 93
  8. theorem OAI.Erdos3.nonprincipalSupport_subset line 107
  9. theorem OAI.Erdos3.nonprincipalSupport_degree line 113
  10. theorem OAI.Erdos3.nonprincipalSupport_card_le line 119
  11. theorem OAI.Erdos3.nonprincipalSupport_abs_sum_le line 126
  12. theorem OAI.Erdos3.rawCanonicalJet_normalized_polynomial line 146