Def CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected

Modification history

2025-10-27 22:34

Mathlib/CategoryTheory/Limits/Shapes/Pullback/Connected.lean

feat(AlgebraicGeometry): global sections of inverse limits of schemes (#30226)

Added CategoryTheory.Limits.isLimitOfIsPullbackOfIsConnected View on Github →