OAI/AlgebraicGeometry/RelativeTriviality/FreeCech.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CampanaPeternellSix.ActualCech.laurent_parts line 13
2. def OAI.CampanaPeternellSix.ActualCech.freeProductIso line 33
3. def OAI.CampanaPeternellSix.ActualCech.freeProjection line 41
4. def OAI.CampanaPeternellSix.ActualCech.freeSectionEquiv line 48
5. lemma OAI.CampanaPeternellSix.ActualCech.freeSectionEquiv_apply line 57
6. lemma OAI.CampanaPeternellSix.ActualCech.freeSectionEquiv_restrict line 72
7. lemma OAI.CampanaPeternellSix.ActualCech.free_ranges_top line 82
8. theorem OAI.CampanaPeternellSix.ActualCech.subsingleton_free_quotient line 113