OAI/Combinatorics/Progressions/Polynomial/PreparedFiniteNestedForwardAllDegreePaddedSource.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.VectorPolynomial.PreparedFiniteNestedForwardAllDegreeSlot line 11
  2. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeOuter line 14
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeStage line 18
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeIsDirect line 22
  5. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeDegree line 26
  6. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeSeed line 30
  7. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor line 35
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeOuter_slot line 40
  9. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeStage_slot line 45
  10. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeIsDirect_slot line 50
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeDegree_slot line 55
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeSeed_slot line 60
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeDegree_le line 67
  14. theorem OAI.Erdos3.VectorPolynomial.le_preparedFiniteNestedForwardAllDegreeSeed line 73
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor_outer line 79
  16. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor_stage line 85
  17. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor_model line 91
  18. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor_degree line 96
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardAllDegreeAnchor_seed line 101
  20. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedForwardAllDegreePaddedProductiveSource line 107