OAI/NumberTheory/PiExponent/Geometry/CurveNormalizationDegree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.CurveNormalizationDegree.cokernel_stalk_subsingleton line 14
2. theorem OAI.PiExponent.CurveNormalizationDegree.finite_closed_complement line 40
3. theorem OAI.PiExponent.CurveNormalizationDegree.stalk_subsingleton_of_localIso line 62
4. theorem OAI.PiExponent.CurveNormalizationDegree.tensor_stalk_subsingleton line 75
5. theorem OAI.PiExponent.CurveNormalizationDegree.finite_support_euler line 82
6. theorem OAI.PiExponent.CurveNormalizationDegree.finite_support_tensor_euler line 102
7. theorem OAI.PiExponent.CurveNormalizationDegree.cokernel_tensor_euler line 124