Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.Scheme.open_cover.ι_from_glued

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.ι_from_gluedView on Github →