OAI/AlgebraicGeometry/Seshadri/Bertini/GenericSmoothness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.BertiniIntegral.hyperplane_parameter_polynomial_ne_zero line 16
2. theorem OAI.MaximalSeshadri.BertiniIntegral.etale_generic_smooth_integral_hyperplane_section line 53
3. theorem OAI.MaximalSeshadri.BertiniIntegral.simultaneous_etale_smooth_integral_hyperplanes line 97
4. def OAI.MaximalSeshadri.BertiniIntegral.hyperplaneVariable line 139
5. def OAI.MaximalSeshadri.BertiniIntegral.permuteHyperplaneHom line 142
6. lemma OAI.MaximalSeshadri.BertiniIntegral.permuteHyperplaneHom_injective line 147
7. lemma OAI.MaximalSeshadri.BertiniIntegral.permuteHyperplaneHom_variable line 153
8. theorem OAI.MaximalSeshadri.BertiniIntegral.simultaneous_reindexed_generic_hyperplane_parameters line 171
9. theorem OAI.MaximalSeshadri.BertiniIntegral.simultaneous_reindexed_smooth_integral_hyperplanes line 209