Documentation
GeometricallyP
.
Mathlib
.
AlgebraicGeometry
.
Morphisms
.
UnderlyingMap
Search
return to top
source
Imports
Init
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Imported by
AlgebraicGeometry
.
instIsMultiplicativeSchemeSurjective_geometricallyP
source
instance
AlgebraicGeometry
.
instIsMultiplicativeSchemeSurjective_geometricallyP
:
CategoryTheory.MorphismProperty.IsMultiplicative
@
Surjective