OAI/Algebra/AlgebraicObstruction/FormalArcs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.complete_principal_powerSeries line 19
  2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.completeDVR_powerSeries line 77
  3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.DVR_completion_powerSeries line 86
  4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.finite_normalization_arc line 131
  5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.finite_powerSeries_curve_arc line 202
  6. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.mem_principal_smul_pi line 244
  7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.principal_pi_precomplete line 258
  8. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.finite_primary_quotient line 283
  9. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.finite_over_parameter line 307
  10. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.primary_parameter_arc line 356