Theorem AlgebraicGeometry.Scheme.Pullback.gluing_ι

Modification history

2025-09-19 16:11

Mathlib/AlgebraicGeometry/Pullbacks.lean

refactor(AlgebraicGeometry): rename fields of `Scheme.Cover` to match `ZeroHypercover` (#29803) …

Modified AlgebraicGeometry.Scheme.Pullback.gluing_ι View on Github →

2024-05-17 23:31

Mathlib/AlgebraicGeometry/Pullbacks.lean

chore: cleanup `AlgebraicGeometry.Pullbacks` (#12995) …

Added AlgebraicGeometry.Scheme.Pullback.gluing_ι View on Github →