Def AlgebraicGeometry.Scheme.Pullback.Triplet.mk'

Modification history

2025-10-15 10:06

Mathlib/AlgebraicGeometry/PullbackCarrier.lean

chore(AlgebraicGeometry): autumn cleaning (#30426) …

Modified AlgebraicGeometry.Scheme.Pullback.Triplet.mk'View on Github →

2024-11-05 11:12

Mathlib/AlgebraicGeometry/PullbackCarrier.lean

feat(AlgebraicGeometry/Pullback): description of the underlying topological space of a fiber product of schemes (#17767) …

Added AlgebraicGeometry.Scheme.Pullback.Triplet.mk'View on Github →