OAI/Algebra/AlgebraicObstruction/SymbolicPowers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.primary_symbolic_cofinal line 14
  2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.primary_symbolic_cofinal_power line 37
  3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.symbolic_denominator_iff line 53
  4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.taylor_kernel_cofinal line 68
  5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.lift_of_coefficients line 85
  6. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.coefficient_zero_eq_reduction line 112
  7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.primitive_approximation_from_constant_reduction line 124