OAI/NumberTheory/PiExponent/Ampleness/AmpleIso.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.AmpleIso.sectionOpen_postcomp_iso line 14
2. theorem OAI.PiExponent.AmpleIso.isAmple_of_sheaf_iso line 19
3. theorem OAI.PiExponent.AmpleIso.isAmple_iff_sheaf_iso line 30