OAI/Combinatorics/Progressions/Lattices/ForecastNativeResidueTest.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastNativeSpatialResidue line 16
  2. theorem OAI.Erdos3.VectorPolynomial.forecastNativeSpatialResidue_output line 20
  3. theorem OAI.Erdos3.VectorPolynomial.forecastNativeSpatialResidue_reduction line 24
  4. def OAI.Erdos3.VectorPolynomial.forecastNativeSheetResidue line 32
  5. def OAI.Erdos3.VectorPolynomial.forecastNativeFreeDeckResidue line 39
  6. def OAI.Erdos3.VectorPolynomial.forecastNativeCoordinateResidue line 43
  7. theorem OAI.Erdos3.VectorPolynomial.forecastNativeCoordinateResidue_output line 50
  8. def OAI.Erdos3.VectorPolynomial.forecastNativeDeckResidueMatrix line 70
  9. theorem OAI.Erdos3.VectorPolynomial.forecastNativeDeckResidueMatrix_bounds line 75
  10. theorem OAI.Erdos3.VectorPolynomial.forecastNativeDeckResidueMatrix_apply line 82
  11. def OAI.Erdos3.VectorPolynomial.forecastNativeAmbientDeckResidue line 91
  12. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientDeckResidue_output line 98
  13. theorem OAI.Erdos3.VectorPolynomial.forecastNativeAmbientDeckResidue_reduction line 114
  14. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastResidueTest line 154
  15. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastResidueTest_bounds line 164
  16. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.forecastResidueTest_eq_eval line 175