OAI/Algebra/AlgebraicObstruction/AlgebraicGerms.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.common_chart_finite line 15
  2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_span_witness line 24
  3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_mul line 60
  4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_square_witness line 75
  5. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.extendDerivation line 105
  6. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.extendDerivation_algebraMap line 110
  7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.etale_derivation_ext line 118
  8. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.polynomial_pderiv_expansion line 140
  9. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localCoeffAlgebra line 151
  10. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localCoeffTower line 154
  11. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localCompletionCoeffTower line 158
  12. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.deriv line 166
  13. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.expansion_deriv line 170
  14. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_pderiv line 188
  15. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.germ line 204
  16. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_polynomial line 211
  17. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_X line 215
  18. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_zero line 218
  19. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_add line 221
  20. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_neg line 236
  21. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_sub line 243
  22. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_sum line 249
  23. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.germ_subst line 260