OAI/Algebra/AlgebraicObstruction/PositiveCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_map line 13
2. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.fullTaylor_map_le_nil line 29
3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.fullTaylor_pow_zero line 42
4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.positive_coefficient_descends line 59
5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.fullTaylor_eq_of_sub_mem line 100
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.fullTaylor_gradient_descends line 114
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.fullTaylor_positive_coefficients line 138
8. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_comp_coefficient line 160
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.reduction_mem_coeff_pow line 166
10. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.finite_algebra_adic_separated line 178
11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.reduction_fullTaylor line 191