Theorem AlgebraicGeometry.Scheme.Hom.isCompact_preimage

Modification history

2026-01-07 00:18

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

feat(AlgebraicGeometry): universal property of relative normalization (#33476)

Modified AlgebraicGeometry.Scheme.Hom.isCompact_preimage View on Github →

2025-12-28 17:51

Mathlib/AlgebraicGeometry/Normalization.lean

feat(AlgebraicGeometry): relative normalization of schemes (#32813)

Added AlgebraicGeometry.Scheme.Hom.isCompact_preimage View on Github →