OAI/Algebra/AlgebraicObstruction/EtaleCoefficients.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.centerPolynomial line 15
2. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pointEval line 20
3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.pderiv_rename_inl line 23
4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.centerPolynomial_derivative line 30
5. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.centerPolynomial_constant line 46
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.centerPolynomial_linear line 58
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.centerPolynomial_solution line 65
8. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_submersive line 98
9. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.seriesCoefficientRing line 169
10. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.nested_polynomial_finite_coefficients line 182
11. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.coefficientsIn_polynomial_eval line 196
12. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_etale_image line 220
13. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_etale_localization line 259
14. structure OAI.BoundaryOnly.FormalObstruction.FormalCorrection.LocalEtaleExpansion line 294
15. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.LocalEtaleExpansion.finite_coefficients line 317
16. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses.finite_ring_etale line 332
17. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.no_etale_quadratic_data line 348