Def AlgebraicGeometry.Scheme.Pullback.Triplet.tensor

Modification history

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.tensor View on Github →