Theorem AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst

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