Commit 2025-04-10 12:30 690c9f41

View on Github →

feat(AlgebraicGeometry): Chevalley's theorem (#23623)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

added theorem AlgebraicGeometry.Scheme.Hom.isConstructible_image

added theorem AlgebraicGeometry.Scheme.Hom.isConstructible_preimage

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added def AlgebraicGeometry.Scheme.Hom.isoOpensRange

added theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι

added theorem AlgebraicGeometry.Scheme.Hom.isoOpensRange_inv_comp