OAI/AlgebraicGeometry/Seshadri/Intersection/OpenChartDegree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Geometry.topIso_baseScalars line 22
2. def OAI.MaximalSeshadri.Geometry.openTopAlgEquiv line 39
3. lemma OAI.MaximalSeshadri.Geometry.chart_topIso_naturality line 53
4. def OAI.MaximalSeshadri.Geometry.structuralOpenChartMap line 62
5. lemma OAI.MaximalSeshadri.Geometry.structuralOpenChartMap_apply line 73
6. lemma OAI.MaximalSeshadri.Geometry.structuralOpenChartMap_ker line 84
7. lemma OAI.MaximalSeshadri.Geometry.structuralOpenChartMap_surjective line 98
8. theorem OAI.MaximalSeshadri.Geometry.IntegralCurve.nodal_branch_sum_le_degree_on_open line 110