OAI/NumberTheory/PiExponent/Jets/TaylorRectangular.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.TaylorRectangular.residueTaylor_mem_rectangular line 17
  2. theorem OAI.PiExponent.TaylorRectangular.residueTaylor_quotient_eq_zero line 26
  3. def OAI.PiExponent.TaylorRectangular.rationalFrame line 35
  4. theorem OAI.PiExponent.TaylorRectangular.rationalFrame_apply line 39
  5. theorem OAI.PiExponent.TaylorRectangular.rationalFrame_commute line 42
  6. def OAI.PiExponent.TaylorRectangular.derivativeWord line 48
  7. theorem OAI.PiExponent.TaylorRectangular.frameWord_append line 52
  8. theorem OAI.PiExponent.TaylorRectangular.frameWord_replicate line 58
  9. theorem OAI.PiExponent.TaylorRectangular.mixedIter_eq_frameWord line 64
  10. theorem OAI.PiExponent.TaylorRectangular.derivativeWord_cost line 75
  11. theorem OAI.PiExponent.TaylorRectangular.derivativeWord_cost_le line 89
  12. theorem OAI.PiExponent.TaylorRectangular.frame_residueTaylor_ideal_le line 101
  13. def OAI.PiExponent.TaylorRectangular.costRectangle line 116
  14. theorem OAI.PiExponent.TaylorRectangular.costRectangle_pos line 120
  15. theorem OAI.PiExponent.TaylorRectangular.costRectangle_budget line 124
  16. theorem OAI.PiExponent.TaylorRectangular.costRectangle_product_lower line 140
  17. theorem OAI.PiExponent.TaylorRectangular.frame_residueTaylor_costRectangle_ideal_le line 156