OAI/Algebra/AlgebraicObstruction/WitnessDescent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.vanishes_mem_origin_pow line 16
  2. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.origin_pow_iff_vanishes line 45
  3. structure OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses line 56
  4. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses.exists line 67
  5. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.subtype_series_map_injective line 89
  6. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses.descend line 95
  7. inductive OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticEntry line 176
  8. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticEntry.variables line 184
  9. instance OAI.BoundaryOnly.FormalObstruction.CoefficientRing.(instance at line 188) line 188
  10. def OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses.entry line 191
  11. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.QuadraticWitnesses.finite_ring line 199
  12. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.no_presented_quadratic_data line 215