OAI/Algebra/FrobeniusObstruction/LiftProducts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundaryOnly.FormalObstruction.ThreeParameters.chosen line 13
2. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.chosen_augmentation line 16
3. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.chosen_square line 21
4. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.chosen_outside line 26
5. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.chosen_product line 34
6. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.separated_parameter_lift_some line 46
7. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.liftScalar line 79
8. def OAI.BoundaryOnly.FormalObstruction.ActualBlocks.liftBlock line 83
9. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.liftBlock_delta line 88
10. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.reduce_liftBlock line 97
11. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.liftScalar_potential line 106
12. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.liftScalar_slope line 114
13. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.reduction_lifted_product line 120
14. theorem OAI.BoundaryOnly.FormalObstruction.ActualBlocks.parameter_cycle line 136