Def AlgebraicGeometry.Scheme.IsLocallyDirected.tAux

Modification history

2025-06-13 16:09

Mathlib/AlgebraicGeometry/Gluing.lean

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

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