OAI/NumberTheory/PiExponent/Geometry/IntegralCurveExistence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NumericalAmpleness.irreducibleClosedRestrict line 12
2. def OAI.PiExponent.NumericalAmpleness.irreducibleClosedsBelowEquiv line 29
3. theorem OAI.PiExponent.NumericalAmpleness.topologicalKrullDim_irreducibleClosed line 59
4. theorem OAI.PiExponent.NumericalAmpleness.exists_irreducibleClosed_dimension_one line 65
5. theorem OAI.PiExponent.NumericalAmpleness.isReduced_vanishingIdeal_subscheme line 81
6. def OAI.PiExponent.NumericalAmpleness.integralCurveOfIrreducibleClosed line 95
7. theorem OAI.PiExponent.NumericalAmpleness.nonempty_integralCurve_of_dimension_pos line 117