OAI/AlgebraicGeometry/Seshadri/Projective/CenteredEmbedding.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.Projective.embedding_reindex_nonemptyline 23 - lemma
OAI.MaximalSeshadri.Projective.exists_centered_embeddingline 39 - lemma
OAI.MaximalSeshadri.Projective.centeredOpen_nonempty_of_singletonline 67