OAI/AlgebraicGeometry/Seshadri/Sheaves/TensorRestrictPure.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.TensorPure.sheafify_restrict_unitline 17 - lemma
OAI.MaximalSeshadri.TensorPure.presheaf_restrict_pureline 39 - lemma
OAI.MaximalSeshadri.TensorPure.restrict_pureline 47