Def algebraic_geometry.Scheme.open_cover.glue_morphisms

Modification history

2022-01-14 13:04
src/algebraic_geometry/gluing.lean
feat(algebraic_geometry): Gluing morphisms from an open cover. (#11441)
Added algebraic_geometry.Scheme.open_cover.glue_morphismsView on Github →