OAI/NumberTheory/PiExponent/Cohomology/EulerSupportDimension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.NumericalAmpleness.dimension_le_of_local_bound line 13
2. theorem OAI.PiExponent.NumericalAmpleness.mono_comp_iso line 38
3. theorem OAI.PiExponent.NumericalAmpleness.mono_iso_inv_comp line 43

   Distinct definitions of this name: OAI/NumberTheory/PiExponent/Ampleness/NakaiCartier.lean:15 (different declaration text), OAI/NumberTheory/PiExponent/Geometry/SectionCartierRegular.lean:12 (different declaration text). Qualify references as OAI.PiExponent.NumericalAmpleness.mono_iso_inv_comp@path.

4. theorem OAI.PiExponent.NumericalAmpleness.section_coefficient_regular line 48
5. theorem OAI.PiExponent.NumericalAmpleness.section_affine_coefficient_nonZeroDivisor line 63
6. theorem OAI.PiExponent.NumericalAmpleness.regular_sectionZero_dimension_le line 72