OAI/Combinatorics/Chromatic/Walls/PolynomialCoeffLinear.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.polynomialCoeffLinear line 12
  2. def OAI.ElementaryPositivity.RawShuffle.relativeCoeffB line 18
  3. lemma OAI.ElementaryPositivity.RawShuffle.relativeCoeffB_tmul line 23
  4. theorem OAI.ElementaryPositivity.RawShuffle.relativeCoeffB_graded line 31
  5. theorem OAI.ElementaryPositivity.RawShuffle.relative_restriction_graded line 68
  6. def OAI.ElementaryPositivity.RawShuffle.polynomialMapLinear line 85
  7. lemma OAI.ElementaryPositivity.RawShuffle.polynomialMapLinear_coeff line 95
  8. lemma OAI.ElementaryPositivity.RawShuffle.eulerForm_add_left line 100
  9. lemma OAI.ElementaryPositivity.RawShuffle.eulerForm_add_right line 106
  10. lemma OAI.ElementaryPositivity.RawShuffle.coeff_single_toMvPolynomial line 111
  11. lemma OAI.ElementaryPositivity.RawShuffle.restrictionTest_leaf_coeff line 120
  12. def OAI.ElementaryPositivity.RawShuffle.relativeLeading line 131
  13. theorem OAI.ElementaryPositivity.RawShuffle.relativeLeading_divisible line 140
  14. theorem OAI.ElementaryPositivity.RawShuffle.relativeLeading_taylor_divisible line 177