Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 16:03 9150268c

View on Github →

feat (algebraic_geometry): Constructions of fibred products of schemes (#11450) This is the first half of the PRs about constructing fibred products of schemes, where we construct all the relevant schemes and morphisms but yet to show that they are actually fibred products.

Estimated changes