OAI/AlgebraicGeometry/Seshadri/Bertini/IntegralSubschemes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_of_integral_open_cover line 12
2. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_subscheme_of_affine_quotients line 44
3. theorem OAI.MaximalSeshadri.BertiniIntegral.subscheme_meets_affine line 85
4. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_subscheme_of_affine_overlap_quotients line 96
5. theorem OAI.MaximalSeshadri.BertiniIntegral.smooth_integral_linear_family line 116
6. lemma OAI.MaximalSeshadri.BertiniIntegral.vanishingIdeal_compl_eq_span line 176
7. theorem OAI.MaximalSeshadri.BertiniIntegral.smooth_integral_zero_family line 198