OAI/AlgebraicGeometry/Seshadri/Sheaves/RestrictTensorMap.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.TensorPure.restrict_pure_invline 17 - lemma
OAI.MaximalSeshadri.TensorPure.restrict_hom_extline 27 - lemma
OAI.MaximalSeshadri.TensorPure.restrict_mapline 40