OAI/NumberTheory/PiExponent/Ampleness/ComponentAmpleDescentIdeal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponentSeshadri.ComponentAmpleDescent.ideal_le_annihilator_closedModule line 11
2. theorem OAI.PiExponentSeshadri.ComponentAmpleDescent.ideal_mul_eq_bot_of_reduced_cover line 33
3. theorem OAI.PiExponentSeshadri.ComponentAmpleDescent.ideal_le_annihilator_closedModule_of_reduced_cover line 38