OAI/Algebra/FiniteTensor/JetSystems.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Scalar finite equations reconstructing every squarefree component and primitive.

  1. def OAI.PD4Tensor.Spreading.assembleBox line 17
  2. theorem OAI.PD4Tensor.Spreading.assembleBox_boxSeries line 21
  3. theorem OAI.PD4Tensor.Spreading.boxCoeff_mul_algebraMap line 24
  4. theorem OAI.PD4Tensor.Spreading.boxSeries_assembleBox line 28
  5. theorem OAI.PD4Tensor.Spreading.boxSeries_ext line 37
  6. theorem OAI.PD4Tensor.Spreading.boxSeries_zero line 44
  7. theorem OAI.PD4Tensor.Spreading.boxSeries_add line 49
  8. theorem OAI.PD4Tensor.Spreading.boxSeries_sub line 54
  9. theorem OAI.PD4Tensor.Spreading.subst_assembleBox line 59
  10. theorem OAI.PD4Tensor.Spreading.boxSeries_subst line 72
  11. def OAI.PD4Tensor.Spreading.centerSeries line 81
  12. theorem OAI.PD4Tensor.Spreading.centerSeries_zero line 84
  13. theorem OAI.PD4Tensor.Spreading.centerFamily_hasSubst line 88
  14. def OAI.PD4Tensor.Spreading.affineUnknown line 92
  15. theorem OAI.PD4Tensor.Spreading.subst_affineUnknown line 95
  16. theorem OAI.PD4Tensor.Spreading.subst_center_affine line 101
  17. abbrev OAI.PD4Tensor.Spreading.LeftUnknown line 116
  18. abbrev OAI.PD4Tensor.Spreading.RightUnknown line 117
  19. abbrev OAI.PD4Tensor.Spreading.LeftEquation line 118
  20. abbrev OAI.PD4Tensor.Spreading.RightEquation line 119
  21. def OAI.PD4Tensor.Spreading.leftOriginal line 126
  22. def OAI.PD4Tensor.Spreading.rightOriginal line 130
  23. def OAI.PD4Tensor.Spreading.universalLeftH line 133
  24. def OAI.PD4Tensor.Spreading.universalLeftP line 138
  25. def OAI.PD4Tensor.Spreading.universalRightG line 143
  26. def OAI.PD4Tensor.Spreading.universalRightP line 147
  27. theorem OAI.PD4Tensor.Spreading.constantCoeff_universalLeftH line 151
  28. theorem OAI.PD4Tensor.Spreading.hasSubst_universalLeftH line 160
  29. theorem OAI.PD4Tensor.Spreading.hasSubst_universalRightG line 166
  30. def OAI.PD4Tensor.Spreading.universalLeftEquation line 174
  31. def OAI.PD4Tensor.Spreading.universalRightEquation line 184
  32. theorem OAI.PD4Tensor.Spreading.eval_universalLeftH line 194
  33. theorem OAI.PD4Tensor.Spreading.eval_universalLeftP line 203
  34. theorem OAI.PD4Tensor.Spreading.eval_universalRightG line 212
  35. theorem OAI.PD4Tensor.Spreading.eval_universalRightP line 217
  36. theorem OAI.PD4Tensor.Spreading.original_solves_left line 222
  37. theorem OAI.PD4Tensor.Spreading.original_solves_right line 243