OAI/Algebra/FormulaHitting/JetMatrix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.jet_eq_zero_iff line 18
  2. theorem OAI.NCHitting.jet_ne_zero_of_order_lt line 28
  3. def OAI.NCHitting.integrationMatrix line 34
  4. theorem OAI.NCHitting.integrationMatrix_apply line 37
  5. theorem OAI.NCHitting.jet_J line 45
  6. theorem OAI.NCHitting.jet_wordSeries line 66
  7. theorem OAI.NCHitting.generator_cast_eq_integrationMatrix line 77
  8. theorem OAI.NCHitting.Formula.jet_wordSum_eq_eval_mulVec line 84
  9. theorem OAI.NCHitting.Formula.eval_ne_zero_of_jet_wordSum_ne_zero line 93
  10. theorem OAI.NCHitting.Formula.jet_series_eq_eval_mulVec line 102
  11. theorem OAI.NCHitting.Formula.eval_ne_zero_of_jet_series_ne_zero line 109
  12. theorem OAI.NCHitting.Formula.eval_generator_ne_zero_of_jet_series_ne_zero line 116