OAI/NumberTheory/PiExponent/Geometry/CurveComponentMultiplicity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CurveCycle.generic_stalk_isArtinian line 10
2. def OAI.PiExponent.CurveCycle.componentMultiplicity line 35
3. theorem OAI.PiExponent.CurveCycle.componentMultiplicity_pos line 39
4. def OAI.PiExponent.CurveCycle.reducedComponent line 46
5. def OAI.PiExponent.CurveCycle.reducedComponentι line 50
6. instance OAI.PiExponent.CurveCycle.reducedComponent_closed line 55
7. instance OAI.PiExponent.CurveCycle.reducedComponent_integral line 62
8. def OAI.PiExponent.CurveCycle.componentCurve line 77