OAI/Combinatorics/Progressions/Polynomial/PreparedFiniteForwardPrescribedDegreeProductiveSource.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleDegreeProductiveSource line 11
  2. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardStageDegree line 198
  3. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardModelSlot_stageDegree line 201
  4. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectionSlot_stageDegree line 205
  5. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardStageDegree_le line 209
  6. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardDegreeProductiveSource line 213
  7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardAnchoredDegreeProductiveSource line 423
  8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardPrescribedDegreeProductiveSource line 630
  9. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTerminalDegree line 826
  10. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTerminalDegree_before line 830
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTerminalDegree_last line 835
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTerminalDegree_anchor line 839
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardTerminalDegree_le line 844