OAI/Algebra/AlgebraicObstruction/TaylorDescent.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.tensorCompletionEquiv_tmul_one line 21
2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.shiftedTargetEquiv_tmul_one line 39
3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.actual_whole_tuple_descends line 53
4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.completedTaylor_eq_zero_iff line 85
5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.actual_primitive_tuple line 103
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionFaithfullyFlat line 126
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.taylor_primitive_tuple line 132
8. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorEquiv_one line 162
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorEquiv_mul line 168
10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorRingEquiv line 186
11. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficientCompletionRingEquiv line 201
12. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficientCompletionRingEquiv_apply line 209
13. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.fullTaylor line 215
14. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.fullTaylor_of line 221