OAI/Algebra/AlgebraicObstruction/FiniteCoefficients.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.coefficientsIn line 15
  2. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.restrictCoefficients line 18
  3. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.map_restrictCoefficients line 21
  4. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.restrictCoefficients_centered line 25
  5. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.restrictCoefficients_vanishes line 31
  6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.coefficientsIn_map line 36
  7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicit_coefficientsIn line 39
  8. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_normalized line 68
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.vanishes_two_of_coeff line 109
  10. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.internalJacobian line 122
  11. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitG line 125
  12. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitL line 129
  13. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitH line 132
  14. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitG_constant line 138
  15. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitG_internal_linear line 143
  16. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitL_centered line 153
  17. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitH_quadratic line 159
  18. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.polynomial_series_sub line 176
  19. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.polynomial_series_sum line 180
  20. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.implicitGH_equation line 184
  21. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_nonsingular line 207
  22. structure OAI.BoundaryOnly.FormalObstruction.FormalCorrection.NonsingularPresentation line 229
  23. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.NonsingularPresentation.finite_coefficients line 241
  24. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_coefficient_family line 269
  25. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.finite_ring_presentations line 295