OAI/AlgebraicGeometry/Seshadri/Nodal/QuadraticDiscriminant.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.QuadraticJets.taylor_mul_squareline 16 - lemma
OAI.MaximalSeshadri.QuadraticJets.discriminant_smulline 33 - lemma
OAI.MaximalSeshadri.QuadraticJets.discriminant_quadraticline 38 - theorem
OAI.MaximalSeshadri.QuadraticJets.quadratic_coefficients_nondegenerateline 66