OAI/Combinatorics/Progressions/Linear/BooleanJetMatrixFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.boundedSiteMatrix line 11
  2. theorem OAI.Erdos3.VectorPolynomial.siteEvaluation_boundedArrayPolynomial line 15
  3. theorem OAI.Erdos3.VectorPolynomial.siteEvaluation_bounded_coefficients line 26
  4. theorem OAI.Erdos3.VectorPolynomial.bounded_site_factorization_to_array line 35
  5. def OAI.Erdos3.booleanJetExtractionMatrix line 56
  6. theorem OAI.Erdos3.booleanJetExtractionMatrix_mulVec line 60
  7. def OAI.Erdos3.boundedCoefficientIntegerExponentEquiv line 72
  8. def OAI.Erdos3.boundedCoefficientJetMatrix line 79
  9. theorem OAI.Erdos3.booleanJetExtractionMatrix_mul_boundedSite line 85
  10. theorem OAI.Erdos3.boundedCoefficientJetMatrix_period line 101