OAI/Combinatorics/Progressions/Estimates/CoveredMixedArrayImage.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetValues line 20
  2. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample_jets line 25
  3. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetValues_law line 44
  4. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetArrays line 82
  5. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetArrays_integer line 88
  6. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetArrays_real line 94
  7. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetValues_eq_mixedImage line 101
  8. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample_mixed_jets line 110
  9. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientJetArrays_quotient_law line 127
  10. def OAI.Erdos3.normalizedLatticeRepresentativeHom line 158
  11. theorem OAI.Erdos3.normalizedLatticeRepresentative_sum_zsmul line 166
  12. theorem OAI.Erdos3.normalizedCoverLift_sum_zsmul line 174
  13. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientCoverLift_jets line 197
  14. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_mixed_jets line 208