OAI/NumberTheory/PiExponent/Geometry/CurveComponentsDimension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveCycle.reducedComponent_dimension line 10
2. def OAI.PiExponent.CurveCycle.componentIntegralCurve line 21
3. theorem OAI.PiExponent.CurveCycle.exists_component_dimension_one line 30
4. theorem OAI.PiExponent.CurveCycle.component_dimension_one_or_zero line 45