OAI/NumberTheory/PiExponent/Jets/DerivativeIdeals.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.DerivativeIdeals.wordDerivative line 13
  2. theorem OAI.PiExponent.DerivativeIdeals.wordDerivative_nil line 16
  3. theorem OAI.PiExponent.DerivativeIdeals.wordDerivative_cons line 19
  4. def OAI.PiExponent.DerivativeIdeals.wordCost line 22
  5. theorem OAI.PiExponent.DerivativeIdeals.wordCost_nil line 24
  6. theorem OAI.PiExponent.DerivativeIdeals.wordCost_cons line 25
  7. theorem OAI.PiExponent.DerivativeIdeals.wordCost_nonneg line 28
  8. def OAI.PiExponent.DerivativeIdeals.derivativeIdeal line 34
  9. theorem OAI.PiExponent.DerivativeIdeals.word_mem_derivativeIdeal line 37
  10. theorem OAI.PiExponent.DerivativeIdeals.derivativeIdeal_mono line 42
  11. theorem OAI.PiExponent.DerivativeIdeals.self_mem_derivativeIdeal line 49
  12. def OAI.PiExponent.DerivativeIdeals.derivativeCore line 53
  13. theorem OAI.PiExponent.DerivativeIdeals.derivation_mem_derivativeIdeal line 69
  14. theorem OAI.PiExponent.DerivativeIdeals.wordDerivative_mem_derivativeIdeal line 84
  15. theorem OAI.PiExponent.DerivativeIdeals.derivative_vanishes_on_persistent_ideal line 96
  16. theorem OAI.PiExponent.DerivativeIdeals.derivativeIdeal_levels_monotone line 107
  17. theorem OAI.PiExponent.DerivativeIdeals.exists_persistent_derivative_component line 114