OAI/Algebra/FormulaHitting/Series.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NCHitting.integral line 16
2. theorem OAI.NCHitting.coeff_integral_zero line 22
3. theorem OAI.NCHitting.coeff_integral_succ line 26
4. theorem OAI.NCHitting.constantCoeff_integral line 31
5. theorem OAI.NCHitting.derivative_integral line 35
6. theorem OAI.NCHitting.integral_unique line 41
7. theorem OAI.NCHitting.integral_zero line 49
8. theorem OAI.NCHitting.integral_add line 54
9. theorem OAI.NCHitting.integral_smul line 62
10. def OAI.NCHitting.kernel line 69
11. theorem OAI.NCHitting.coeff_kernel line 73
12. def OAI.NCHitting.J line 77
13. theorem OAI.NCHitting.derivative_J line 79
14. theorem OAI.NCHitting.constantCoeff_J line 83
15. theorem OAI.NCHitting.J_zero line 87
16. theorem OAI.NCHitting.J_add line 90
17. theorem OAI.NCHitting.J_smul line 94
18. def OAI.NCHitting.JLinear line 97
19. theorem OAI.NCHitting.J_sum line 103
20. theorem OAI.NCHitting.coeff_J line 108
21. theorem OAI.NCHitting.coeff_J_eq_zero line 126
22. theorem OAI.NCHitting.kernel_mul_linear line 134
23. def OAI.NCHitting.wordSeries line 151
24. theorem OAI.NCHitting.wordSeries_nil line 156
25. theorem OAI.NCHitting.wordSeries_cons line 158
26. theorem OAI.NCHitting.derivative_wordSeries_cons line 161
27. theorem OAI.NCHitting.constantCoeff_wordSeries_cons line 165
28. theorem OAI.NCHitting.coeff_wordSeries_below line 169
29. theorem OAI.NCHitting.length_le_order_wordSeries line 182
30. theorem OAI.NCHitting.map_integral line 190
31. theorem OAI.NCHitting.map_kernel line 198
32. theorem OAI.NCHitting.map_J line 204
33. theorem OAI.NCHitting.map_wordSeries line 209