OAI/Algebra/AlgebraicObstruction/TaylorDifferential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.shiftDeriv_taylor line 17
  2. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionDeriv line 86
  3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionDeriv_of line 92
  4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionDeriv_mem_pow line 100
  5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.shiftDeriv_map line 123
  6. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficient_adic_separated line 133
  7. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionNoetherian line 149
  8. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.additive_eq_of_approximation line 158
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.fullTaylor_deriv_of line 179
  10. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.fullTaylor_deriv line 190