OAI/Algebra/AlgebraicObstruction/LocalOrigin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.origin line 14
2. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.(instance at line 15) line 15
3. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.point_liesOver line 17
4. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.originAlgebra line 26
5. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.originLiesOverAlgebra line 30
6. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.origin_isLocalHom line 35
7. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.maximalIdeal_eq_map_origin line 41