OAI/AlgebraicGeometry/RelativeTriviality/Frames.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CampanaPeternellSix.RelativeCech.clear_residue_denominator line 12
2. lemma OAI.CampanaPeternellSix.RelativeCech.clear_section_denominator line 24
3. theorem OAI.CampanaPeternellSix.RelativeCech.clear_finite_sections_denominator line 48
4. def OAI.CampanaPeternellSix.FiberFrame.sectionsTopEquiv line 66
5. lemma OAI.CampanaPeternellSix.FiberFrame.sectionsTopEquiv_naturality line 80
6. lemma OAI.CampanaPeternellSix.FiberFrame.sectionsTopEquiv_symm_apply line 82
7. instance OAI.CampanaPeternellSix.FiberFrame.inverseOpens_final line 91
8. abbrev OAI.CampanaPeternellSix.FiberFrame.pullbackFreeIso line 102
9. lemma OAI.CampanaPeternellSix.FiberFrame.pullbackFree_sections line 107
10. lemma OAI.CampanaPeternellSix.FiberFrame.pullbackFree_top line 146
11. def OAI.CampanaPeternellSix.FiberFrame.scalarEnd line 164
12. lemma OAI.CampanaPeternellSix.FiberFrame.scalarEnd_app line 187
13. lemma OAI.CampanaPeternellSix.FiberFrame.scalarEnd_app_top line 190
14. lemma OAI.CampanaPeternellSix.FiberFrame.scalarEnd_mul line 194
15. lemma OAI.CampanaPeternellSix.FiberFrame.scalarEnd_one line 200
16. def OAI.CampanaPeternellSix.FiberFrame.scalarIso line 205