OAI/AlgebraicGeometry/Seshadri/Bertini/SimultaneousHyperplanes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.BertiniIntegral.generic_hyperplane_section_over_model line 16
2. theorem OAI.MaximalSeshadri.BertiniIntegral.generic_hyperplane_section line 48
3. theorem OAI.MaximalSeshadri.BertiniIntegral.etale_generic_hyperplane_section line 73
4. def OAI.MaximalSeshadri.BertiniIntegral.restrictHyperplaneHom line 133
5. lemma OAI.MaximalSeshadri.BertiniIntegral.restrictHyperplaneHom_injective line 142
6. lemma OAI.MaximalSeshadri.BertiniIntegral.restrictHyperplaneHom_X line 147
7. lemma OAI.MaximalSeshadri.BertiniIntegral.restrictHyperplaneHom_CX line 152
8. theorem OAI.MaximalSeshadri.BertiniIntegral.common_hyperplane_field line 158
9. theorem OAI.MaximalSeshadri.BertiniIntegral.simultaneous_generic_hyperplane_parameters line 172
10. theorem OAI.MaximalSeshadri.BertiniIntegral.independent_hyperplane_parameters line 187
11. theorem OAI.MaximalSeshadri.BertiniIntegral.simultaneous_etale_integral_hyperplanes line 212