noncomputable def ProjectiveSpace (n : Type v) (S : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme

The projective space over a scheme S, with homogeneous coordinates indexed by n

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.«termℙ(_;_)» : Lean.ParserDescr

ℙ(n; S) is the affine S indexed by n

Equations

• One or more equations did not get rendered due to their size.