Def AlgebraicGeometry.Scheme.IsLocallyDirected.t

Modification history

2025-06-13 16:09

Mathlib/AlgebraicGeometry/Gluing.lean

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

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