OAI/NumberTheory/PiExponent/Ampleness/ReesRelativeSections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.InvertibleLocal.frame_ideal line 14
2. theorem OAI.PiExponentSeshadri.ReesGrading.mono_inv_comp line 40
3. theorem OAI.PiExponentSeshadri.ReesGrading.map_comp_through line 45
4. theorem OAI.PiExponentSeshadri.ReesGrading.relative_generator_section line 57
5. theorem OAI.PiExponentSeshadri.ReesGrading.relative_generator_section_open line 86
6. theorem OAI.PiExponentSeshadri.ReesGrading.relative_affine_section_cover line 148