OAI/Combinatorics/Progressions/Estimates/HomogenizedModeFactorization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.homogeneous_degreeLE line 11
  2. theorem OAI.Erdos3.VectorPolynomial.dehomogenize_degreeLE line 18
  3. theorem OAI.Erdos3.VectorPolynomial.siteEvaluation_homogenize line 30
  4. theorem OAI.Erdos3.VectorPolynomial.siteEvaluation_dehomogenize line 36
  5. theorem OAI.Erdos3.VectorPolynomial.homogeneous_site_factorization_iff line 47