OAI/Combinatorics/Progressions/Lattices/LayerSamplingRankAffine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.monomialScale_const_mul_degree line 13
  2. theorem OAI.Erdos3.monomialScale_le_const_mul line 19
  3. theorem OAI.Erdos3.PolynomialRationalApproximation.homogeneous_dilation_pullback line 26
  4. theorem OAI.Erdos3.PolynomialRationalApproximation.homogeneous_dilation_pullback_max line 71
  5. theorem OAI.Erdos3.PolynomialRationalApproximation.affine_pullback line 85
  6. theorem OAI.Erdos3.PolynomialRationalApproximation.affine_pullback_max line 98
  7. theorem OAI.Erdos3.residueAffinePolynomial_eval_real line 121
  8. def OAI.Erdos3.VectorPolynomial.residueAffine line 136
  9. theorem OAI.Erdos3.VectorPolynomial.eval_residueAffine line 141
  10. theorem OAI.Erdos3.VectorPolynomial.integerRowPolynomial_residueAffine line 147
  11. theorem OAI.Erdos3.HasLayerSamplingRank.residueAffine line 158
  12. theorem OAI.Erdos3.HasLayerSamplingRank.residueAffine_homogeneousPart line 185