OAI/Algebra/AlgebraicObstruction/TaylorTarget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.sup_pow_pred_le line 12
2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.shifted_ideal_cofinal line 24
3. abbrev OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.variablesIdeal line 43
4. abbrev OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.Ring line 44
5. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.mk line 46
6. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.nilIdeal line 48
7. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.variables_pow line 50
8. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.variables_fg line 54
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.variables_ker line 57
10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction line 71
11. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_mk line 77
12. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_surjective line 80
13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_ker line 84
14. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.finite_shifted line 96