OAI/Algebra/AlgebraicObstruction/Differentiation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.mul line 14
2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.pderiv line 21
3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.pderiv line 30
4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.jet_trunc line 35
5. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Jet.subst_series line 41
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.Vanishes.subst line 52
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.derivation_aeval line 59
8. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pderiv_subst_polynomial line 72
9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pderiv_subst line 79