OAI/AlgebraicGeometry/LogKodaira/SmoothCharts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ReverseLogKodaira.SmoothDimension.smooth_dimension_unique line 14
2. theorem OAI.ReverseLogKodaira.SmoothDimension.smooth_relative_dimension_subtraction line 72
3. theorem OAI.ReverseLogKodaira.RelativeCharts.exists_standard_chart_over_smooth_open line 129
4. lemma OAI.ReverseLogKodaira.RelativeCharts.smooth_dimension_restrict_le line 183
5. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.exists_relative_log_chart line 200
6. theorem OAI.ReverseLogKodaira.SmoothDimension.smooth_fiber_dimension line 253