OAI/NumberTheory/PiExponent/Jets/OrdinaryTaylor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.OrdinaryTaylor.wordDerivative_append line 16
  2. theorem OAI.PiExponent.OrdinaryTaylor.wordDerivative_replicate line 23
  3. theorem OAI.PiExponent.OrdinaryTaylor.mixedIter_eq_wordDerivative line 30
  4. theorem OAI.PiExponent.OrdinaryTaylor.derivativeWord_wordCost line 40
  5. theorem OAI.PiExponent.OrdinaryTaylor.derivativeWord_wordCost_le line 54
  6. theorem OAI.PiExponent.OrdinaryTaylor.residueTaylor_ideal_le line 66
  7. theorem OAI.PiExponent.OrdinaryTaylor.persistent_ideal_le line 81
  8. def OAI.PiExponent.OrdinaryTaylor.ordinaryTaylor line 98
  9. theorem OAI.PiExponent.OrdinaryTaylor.ordinaryTaylor_constant line 104
  10. theorem OAI.PiExponent.OrdinaryTaylor.ordinaryTaylor_firstCoefficient line 110
  11. theorem OAI.PiExponent.OrdinaryTaylor.mixedIter_eq_ordinaryWord line 117
  12. theorem OAI.PiExponent.OrdinaryTaylor.ordinaryTaylor_ideal_le line 123
  13. theorem OAI.PiExponent.OrdinaryTaylor.ordinary_residueTaylor_ideal_le line 133
  14. theorem OAI.PiExponent.OrdinaryTaylor.ordinary_persistent_ideal_le line 144