Def AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit

Modification history

2025-06-13 16:09

Mathlib/AlgebraicGeometry/Gluing.lean

feat(AlgebraicGeometry): locally directed gluing (#24796)

Added AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit View on Github →