OAI/Algebra/AlgebraicObstruction/TaylorEvaluation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.Trunc line 15
2. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.reduction line 17
3. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.reduction_surjective line 21
4. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.reduction_ker_pow line 26
5. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.sectionMap line 32
6. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.reduction_sectionMap line 41
7. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.ResidueSection.reduction_mk line 49
8. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.poly line 60
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.variables_map_le line 66
10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.evaluate line 74
11. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.evaluate_mk line 83
12. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.evaluate_shift line 89
13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.reduction_evaluate line 110
14. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorEvaluate.evaluate_taylor line 126
15. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SymbolicTaylor.kernel_le_symbolic line 160