Def algebraic_geometry.Scheme.glue_data.open_cover

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.glue_data.open_cover View on Github →