OAI/Combinatorics/Progressions/Polynomial/RawAffinePolynomialJet.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realJetMatrix_sumColumns line 14
  2. theorem OAI.Erdos3.affineJetUnitMap_monomial_jet line 23
  3. theorem OAI.Erdos3.affineJetUnitMap_raw_monomial_jet line 50
  4. theorem OAI.Erdos3.monomialArrayPolynomial_equiv line 83
  5. def OAI.Erdos3.originalMonomialJetMap line 89
  6. theorem OAI.Erdos3.originalMonomialJetMap_measurable_comp line 96
  7. theorem OAI.Erdos3.originalMonomialJetMap_eq_affine line 114
  8. theorem OAI.Erdos3.originalMonomialJetMap_unit_law line 144
  9. def OAI.Erdos3.rawAffinePolynomialJet line 193
  10. theorem OAI.Erdos3.rawAffinePolynomialJet_eq_affine line 198
  11. theorem OAI.Erdos3.rawAffinePolynomialJet_unit_law line 222