Theorem AlgebraicGeometry.isPullback_Spec_map_pushout

Modification history

2024-11-04 13:07
Mathlib/AlgebraicGeometry/Pullbacks.lean
feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback (#18255)
Added AlgebraicGeometry.isPullback_Spec_map_pushoutView on Github →