OAI/Algebra/FormulaHitting/Wronskian.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.derivativeIter line 17
  2. theorem OAI.NCHitting.derivativeIter_zero line 21
  3. theorem OAI.NCHitting.derivativeIter_add line 23
  4. theorem OAI.NCHitting.derivativeIter_smul line 29
  5. theorem OAI.NCHitting.derivativeIter_sum line 35
  6. theorem OAI.NCHitting.coeff_derivativeIter line 41
  7. theorem OAI.NCHitting.coeff_X_pow_derivativeIter line 54
  8. def OAI.NCHitting.derivativeTail line 62
  9. theorem OAI.NCHitting.coeff_derivativeTail line 65
  10. theorem OAI.NCHitting.X_pow_derivativeIter_eq line 70
  11. def OAI.NCHitting.wronskianMatrix line 80
  12. def OAI.NCHitting.wronskian line 84
  13. theorem OAI.NCHitting.wronskian_linearCombination line 87
  14. def OAI.NCHitting.normalizedWronskianMatrix line 105
  15. theorem OAI.NCHitting.wronskianMatrix_scaling line 109
  16. theorem OAI.NCHitting.wronskian_det_scaling line 120
  17. theorem OAI.NCHitting.det_descFactorial line 128
  18. theorem OAI.NCHitting.det_descFactorial_ne_zero line 139
  19. theorem OAI.NCHitting.normalizedWronskian_constant_ne_zero line 146
  20. theorem OAI.NCHitting.wronskian_order_sum line 163