OAI/Algebra/AlgebraicObstruction/RadicalPrimitives.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.substitution_pderiv_polynomial line 17
  2. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.continuous_pderiv line 39
  3. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.substitution_pderiv line 47
  4. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.constantCoeff_subst_centered line 63
  5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.primitive_constant_on_arc line 71
  6. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.radical_primitive_constant line 96
  7. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.chartCoeffAlgebra line 167
  8. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.chartCoeffTower line 169
  9. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.pointAlgHom line 172
  10. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.radical_extended line 179
  11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.primitive_constant_reduction line 190
  12. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.primitive_approximation line 241