OAI/Combinatorics/Chromatic/Shuffle/BothTaylorB.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.polynomial_eq_of_rat_evals line 13
  2. lemma OAI.ElementaryPositivity.RawShuffle.taylorB_eval line 23
  3. lemma OAI.ElementaryPositivity.RawShuffle.tensorValue_translation line 33
  4. lemma OAI.ElementaryPositivity.RawShuffle.restrictTensor_translation line 42
  5. lemma OAI.ElementaryPositivity.RawShuffle.restrictionB_translation line 49
  6. lemma OAI.ElementaryPositivity.RawShuffle.polynomialMapLinear_monomial line 67
  7. lemma OAI.ElementaryPositivity.RawShuffle.polynomialMapLinear_eval_rat line 74
  8. def OAI.ElementaryPositivity.RawShuffle.bothTaylorB line 83
  9. def OAI.ElementaryPositivity.RawShuffle.evalTwo line 95
  10. lemma OAI.ElementaryPositivity.RawShuffle.bothTaylorB_eval line 99
  11. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylorB_eval line 124
  12. lemma OAI.ElementaryPositivity.RawShuffle.evalTwo_ext line 139
  13. def OAI.ElementaryPositivity.RawShuffle.bothLeading line 147
  14. def OAI.ElementaryPositivity.RawShuffle.commonRelativeLeading line 156
  15. lemma OAI.ElementaryPositivity.RawShuffle.bothLeading_eval line 165
  16. lemma OAI.ElementaryPositivity.RawShuffle.commonRelativeLeading_eval line 178
  17. lemma OAI.ElementaryPositivity.RawShuffle.bothLeading_relative line 193
  18. theorem OAI.ElementaryPositivity.RawShuffle.bothLeading_diagonal_divisible line 210