OAI/Algebra/AlgebraicObstruction/TaylorCompletion.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.completionAlgEquiv line 19
  2. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.tensorCompletionEquiv line 32
  3. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.tensorCompletionEquiv_one_tmul line 46
  4. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.polynomialTensor_X line 69
  5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.polynomialTensor_ideal line 80
  6. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.tensorTruncateEquiv line 102
  7. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.map_variables line 111
  8. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.mapEquiv line 119
  9. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.quotientTensorTruncateEquiv line 124
  10. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.mapAlgEquiv line 136
  11. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.quotientTensorTruncateAlgEquiv line 142
  12. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficient_eq_algebraMap line 158
  13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficient_finite line 161
  14. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficientCompletionEquiv line 167
  15. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.shiftedTargetEquiv line 178
  16. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.map line 201
  17. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.map_mk line 205
  18. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.quotientCoefficient line 208
  19. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.tensorQuotient_coefficient line 212
  20. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorTarget.quotientTensorTruncateAlgEquiv_one_tmul line 220
  21. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.coefficientCompletionEquiv_of line 243
  22. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.shiftedTargetEquiv_one_tmul line 261
  23. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.equiv_smul_of line 283
  24. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorEquiv_tmul line 311
  25. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.completedTaylor line 328
  26. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.TaylorShift.completedTaylor_of line 335