Def algebraic_geometry.Scheme.open_cover.pullback_cover

Modification history

2022-01-14 10:07
src/algebraic_geometry/open_immersion.lean
feat(algebraic_geometry/open_immersion): Operations on open covers. (#11442)
Added algebraic_geometry.Scheme.open_cover.pullback_coverView on Github →