OAI/AlgebraicGeometry/RelativeTriviality/GlobalFunctions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.laurent_coeff_nat line 16
2. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.laurent_coeff_neg line 20
3. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.polynomial_overlap_constants line 28
4. def OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.scalars line 55
5. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.scalars_restrict_X line 58
6. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.scalars_left line 71
7. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.scalars_right line 79
8. lemma OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.polynomial_restrictions_agree line 90
9. theorem OAI.CampanaPeternellSix.RelativeLineGlobalFunctions.scalars_bijective line 98