OAI/NumberTheory/PiExponent/Jets/CommutingTaylor.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CommutingTaylor.iter line 11
  2. theorem OAI.PiExponent.CommutingTaylor.iter_zero line 13
  3. theorem OAI.PiExponent.CommutingTaylor.iter_succ line 14
  4. theorem OAI.PiExponent.CommutingTaylor.iter_mul line 25
  5. theorem OAI.PiExponent.CommutingTaylor.factorial_normalize line 41
  6. def OAI.PiExponent.CommutingTaylor.taylorSeries line 55
  7. theorem OAI.PiExponent.CommutingTaylor.coeff_taylorSeries line 58
  8. theorem OAI.PiExponent.CommutingTaylor.taylorSeries_mul line 62
  9. def OAI.PiExponent.CommutingTaylor.taylorHom line 73
  10. theorem OAI.PiExponent.CommutingTaylor.coeff_taylorHom line 89
  11. theorem OAI.PiExponent.CommutingTaylor.constantCoeff_taylorHom line 93
  12. def OAI.PiExponent.CommutingTaylor.mixedIter line 98
  13. def OAI.PiExponent.CommutingTaylor.taylorHomFin line 102
  14. theorem OAI.PiExponent.CommutingTaylor.coeff_taylorHomFin line 107
  15. theorem OAI.PiExponent.CommutingTaylor.mixedIter_zero line 130
  16. theorem OAI.PiExponent.CommutingTaylor.mixedIter_single line 138
  17. theorem OAI.PiExponent.CommutingTaylor.coeff_zero_taylorHomFin line 149
  18. theorem OAI.PiExponent.CommutingTaylor.coeff_single_taylorHomFin line 153
  19. def OAI.PiExponent.CommutingTaylor.residueTaylorFin line 163
  20. theorem OAI.PiExponent.CommutingTaylor.coeff_residueTaylorFin line 168
  21. theorem OAI.PiExponent.CommutingTaylor.coeff_zero_residueTaylorFin line 175
  22. theorem OAI.PiExponent.CommutingTaylor.coeff_single_residueTaylorFin line 180
  23. theorem OAI.PiExponent.CommutingTaylor.constantCoeff_residueTaylorFin line 185
  24. theorem OAI.PiExponent.CommutingTaylor.constantCoeff_comp_residueTaylorFin line 191
  25. theorem OAI.PiExponent.CommutingTaylor.iter_commute line 197
  26. theorem OAI.PiExponent.CommutingTaylor.mixedIter_commute line 202