OAI/AlgebraicGeometry/Seshadri/Sheaves/TensorOpenSquare.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.OpenBaseChange.modules_comp_appline 19 - lemma
OAI.MaximalSeshadri.OpenBaseChange.hom_appline 22 - lemma
OAI.MaximalSeshadri.OpenBaseChange.tensor_pureline 43 - lemma
OAI.MaximalSeshadri.OpenBaseChange.tensor_squareline 59