OAI/Combinatorics/Chromatic/Walls/Taylor.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ElementaryPositivity.CommonTranslation.coefficients_mem line 12
  2. theorem OAI.ElementaryPositivity.CommonTranslation.polynomial_coeff_mem line 29
  3. def OAI.ElementaryPositivity.CommonTranslation.taylor line 48
  4. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_X line 51
  5. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_C line 54
  6. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_eval line 58
  7. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_coeff_zero line 65
  8. def OAI.ElementaryPositivity.CommonTranslation.D line 70
  9. lemma OAI.ElementaryPositivity.CommonTranslation.D_X line 73
  10. lemma OAI.ElementaryPositivity.CommonTranslation.D_C line 74
  11. lemma OAI.ElementaryPositivity.CommonTranslation.D_mul line 75
  12. lemma OAI.ElementaryPositivity.CommonTranslation.D_eq_sum line 78
  13. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_derivative line 87
  14. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_coeff_one line 97
  15. lemma OAI.ElementaryPositivity.CommonTranslation.D_rename line 101
  16. theorem OAI.ElementaryPositivity.CommonTranslation.D_mem_of_translation_mem line 108
  17. lemma OAI.ElementaryPositivity.CommonTranslation.taylor_iterate_D line 114
  18. theorem OAI.ElementaryPositivity.CommonTranslation.locally_nilpotent_D line 123