OAI/AlgebraicGeometry/RelativeTriviality/ProjectiveLine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CampanaPeternellSix.RelativeTriviality.grading line 12
2. def OAI.CampanaPeternellSix.RelativeTriviality.line line 13
3. def OAI.CampanaPeternellSix.RelativeTriviality.constants line 14
4. def OAI.CampanaPeternellSix.RelativeTriviality.toBase line 20
5. def OAI.CampanaPeternellSix.RelativeTriviality.fiberProjection line 23
6. def OAI.CampanaPeternellSix.RelativeTriviality.awayProjection line 27
7. instance OAI.CampanaPeternellSix.RelativeTriviality.constants_isIso line 31
8. instance OAI.CampanaPeternellSix.RelativeTriviality.line_toBase_universallyClosed line 40