mathlib3

9150268c - feat (algebraic_geometry): Constructions of fibred products of schemes (#11450)

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. Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>