OAI/Combinatorics/Progressions/Polynomial/PreparedFiniteForwardAllDegreePaddedSource.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.VectorPolynomial.PreparedFiniteForwardAllDegreeSlot line 11
  2. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeStage line 14
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeIsDirect line 17
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeDegree line 20
  5. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeAnchor line 23
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeStage_slot line 27
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeIsDirect_slot line 31
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeDegree_slot line 35
  9. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeDegree_le line 39
  10. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeAnchor_stage line 44
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeAnchor_model line 48
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardAllDegreeAnchor_degree line 52
  13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardAllDegreePaddedProductiveSource line 56