OAI/NumberTheory/PiExponent/Ampleness/NakaiCartier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.NumericalAmpleness.mono_iso_inv_comp line 15

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

2. def OAI.PiExponent.NumericalAmpleness.cartierPowerMultiply line 18
3. theorem OAI.PiExponent.NumericalAmpleness.cartierPowerMultiply_mono line 23
4. def OAI.PiExponent.NumericalAmpleness.cartierPowerQuotient line 32
5. def OAI.PiExponent.NumericalAmpleness.cartierPowerSequence line 35
6. theorem OAI.PiExponent.NumericalAmpleness.cartierPowerSequence_shortExact line 39
7. theorem OAI.PiExponent.NumericalAmpleness.cartierPowerMultiply_restrict_isIso line 47
8. theorem OAI.PiExponent.NumericalAmpleness.cartierPowerQuotient_restrict_isZero line 60
9. theorem OAI.PiExponent.NumericalAmpleness.eventual_cartierPower_sections_lift line 75