OAI/AlgebraicGeometry/Seshadri/Bertini/EtaleCoordinates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.BertiniIntegral.mem_principal_smul_top_iff_dvd line 13
2. lemma OAI.MaximalSeshadri.BertiniIntegral.weaklyRegular_pair_iff line 18
3. theorem OAI.MaximalSeshadri.BertiniIntegral.flat_regular_pair line 26
4. theorem OAI.MaximalSeshadri.BertiniIntegral.flat_plane_coordinates line 35
5. abbrev OAI.MaximalSeshadri.BertiniIntegral.coordinateDifference line 61
6. abbrev OAI.MaximalSeshadri.BertiniIntegral.coordinateSum line 66
7. abbrev OAI.MaximalSeshadri.BertiniIntegral.shearMinus line 71
8. abbrev OAI.MaximalSeshadri.BertiniIntegral.shearPlus line 76
9. lemma OAI.MaximalSeshadri.BertiniIntegral.shearMinus_plus line 81
10. lemma OAI.MaximalSeshadri.BertiniIntegral.shearPlus_minus line 91
11. def OAI.MaximalSeshadri.BertiniIntegral.shearEquiv line 101
12. theorem OAI.MaximalSeshadri.BertiniIntegral.coordinateDifference_flat line 105
13. def OAI.MaximalSeshadri.BertiniIntegral.chartDifference line 120
14. lemma OAI.MaximalSeshadri.BertiniIntegral.chartDifference_X line 124
15. theorem OAI.MaximalSeshadri.BertiniIntegral.chartDifference_flat line 130
16. theorem OAI.MaximalSeshadri.BertiniIntegral.chartDifference_regular_pair line 141
17. def OAI.MaximalSeshadri.BertiniIntegral.etaleCotangentCoordinate line 176
18. theorem OAI.MaximalSeshadri.BertiniIntegral.etaleCotangentCoordinate_X line 180
19. theorem OAI.MaximalSeshadri.BertiniIntegral.etale_hyperplane_geometricGeneric line 196