Theorem AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι

Modification history

2026-02-06 11:03
Mathlib/AlgebraicGeometry/RelativeGluing.lean
feat(AlgebraicGeometry): replace `PreservesLocalization` with `Coequifibered` (#34701)
Added AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ιView on Github →