OAI/AlgebraicGeometry/LogKodaira/LogLattice.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ReverseLogKodaira.LocalizationLattice.lattice_locality line 16
2. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.basic_functionField_tower line 56
3. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.basic_constants_tower line 68
4. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.regularLattice_basic line 84
5. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.regularLattice_basic_locality line 100
6. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.regularLattice_restriction line 136
7. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.regularLattice_locality line 160
8. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.isLogPluriform_local_iff line 180