OAI/AlgebraicGeometry/LogKodaira/NonzeroFiber.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.CanonicalSpecialization.pluricanonicalCoordinate line 15
2. theorem OAI.ReverseLogKodaira.CanonicalSpecialization.specialize_ne_zero_of_coefficient line 33
3. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.tensorKaehlerEquiv_one_tmul line 83
4. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.exists_compatible_cotangent_basis line 100
5. theorem OAI.ReverseLogKodaira.FiberChartSpecialization.logarithmicNumerator_ne_zero_of_coefficient line 134
6. theorem OAI.ReverseLogKodaira.RelativeCharts.exists_standard_chart_fixed_base line 206
7. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.exists_cotangent_chart line 251
8. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.generic_mem_complement line 287
9. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.generic_mem_basicOpen line 308
10. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.chartToFunctionField_ne_zero_of_mem_basicOpen line 318
11. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.exists_open_meeting_coefficient line 339
12. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.degreeTransport_trans line 387
13. def OAI.ReverseLogKodaira.DifferentialBaseChange.basisDegreeTransport line 394
14. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.pluricanonicalCoordinate_degreeTransport line 403
15. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.base_dimension_le_of_smooth_point line 419
16. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.exists_open_nonzero_fiber_pluriform line 449