OAI/Algebra/AlgebraicObstruction/ChartTruncation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.origin_eq_variables line 17
  2. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.maximalIdeal_eq_map_variables line 21
  3. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.augmentation line 26
  4. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.augmentation_polynomial line 29
  5. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.augmentation_ker line 36
  6. abbrev OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.FormalTruncation line 53
  7. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.formalTruncate line 55
  8. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.reduction_formalTruncate line 59
  9. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncate line 64
  10. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncate_polynomial line 68
  11. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.reduction_truncate line 73
  12. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncate_maximal_pow line 77
  13. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncateQuotient line 85
  14. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.polynomialQuotient line 90
  15. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncate_polynomialQuotient line 99
  16. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.factor_polynomial_truncate line 106
  17. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.polynomial_truncate line 124
  18. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncatedEquiv line 154
  19. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncatedEquiv_mk line 165