OAI/AlgebraicGeometry/Seshadri/Jets/CenteredJetChart.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Projective.affineSectionRatios line 19
2. lemma OAI.MaximalSeshadri.Projective.affineSectionRatios_none line 25
3. lemma OAI.MaximalSeshadri.Projective.sectionsMorphism_affine_ratios line 30
4. lemma OAI.MaximalSeshadri.Projective.etale_reindex line 62
5. lemma OAI.MaximalSeshadri.Projective.cast_chart_factor line 72
6. lemma OAI.MaximalSeshadri.Projective.cast_chart_coordinate line 83
7. theorem OAI.MaximalSeshadri.Projective.exists_centered_etale_ratios line 89