OAI/AlgebraicGeometry/Seshadri/Projective/BertiniEquations.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MaximalSeshadri.BertiniIntegral.smooth_integral_zero_family_with_equationsline 19 - theorem
OAI.MaximalSeshadri.BertiniIntegral.smooth_integral_hyperplane_of_etale_atlas_with_equationsline 81