OAI/Algebra/AlgebraicObstruction/QuadraticData.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.plusCoordinates_centered line 16
2. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.minusCoordinates_centered line 19
3. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.potential_vanishes line 23
4. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graphCoordinates_centered line 30
5. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.correctedGraph line 38
6. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.graph_corrected line 41
7. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.negativeAmbient line 47
8. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.subst_negativeAmbient line 51
9. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.complementaryMatrix_jet line 61
10. structure OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticData line 68
11. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticData.correct line 81
12. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.no_integral_quadratic_data line 126