OAI/AlgebraicGeometry/RelativeTriviality/LocallyFree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CampanaPeternellSix.RelativeCech.free_free_evaluation line 16
2. lemma OAI.CampanaPeternellSix.RelativeCech.free_sections_of_le_frame line 32
3. lemma OAI.CampanaPeternellSix.RelativeCech.flat_of_semilinearEquiv line 53
4. lemma OAI.CampanaPeternellSix.RelativeCech.free_restriction_sections line 72
5. theorem OAI.CampanaPeternellSix.RelativeCech.flat_affine_restriction line 88
6. lemma OAI.CampanaPeternellSix.RelativeCech.flat_affine_image line 134
7. lemma OAI.CampanaPeternellSix.RelativeCech.flat_affine_open line 153
8. theorem OAI.CampanaPeternellSix.RelativeCech.finitePresentation_affine_restriction line 163