OAI/AlgebraicGeometry/Seshadri/Sheaves/TensorCurveEuler.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Geometry.tensor_multiply_isoOpenline 18 - lemma
OAI.MaximalSeshadri.Geometry.tensor_multiply_shortExactline 44 - theorem
OAI.MaximalSeshadri.Geometry.tensor_multiply_cokernel_flasqueline 52 - lemma
OAI.MaximalSeshadri.Geometry.tensor_multiply_cokernel_ext_zeroline 81 - theorem
OAI.MaximalSeshadri.Geometry.projective_tensor_cokernel_finiteline 92 - theorem
OAI.MaximalSeshadri.Geometry.projective_tensor_euler_differenceline 133