OAI/Algebra/AlgebraicObstruction/Holonomy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryOnly.Holonomy.triple_mem_cube line 14
2. lemma OAI.BoundaryOnly.Holonomy.cube_iSup_le_of_le_deviation line 19
3. lemma OAI.BoundaryOnly.Holonomy.pow_sup_defect_le line 25
4. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.origin_eq_maximal line 45
5. lemma OAI.BoundaryOnly.FormalObstruction.CoefficientRing.gradientIdeal_le_origin line 52
6. theorem OAI.BoundaryOnly.FormalObstruction.CoefficientRing.no_holonomy_algebraic_input line 67