Commit 2026-01-20 22:17 93f17ae8

View on Github →

chore(AlgebraicGeometry): rename fields in classes (#34180)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.isClosedEmbedding

Modified Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Integral.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

deleted theorem AlgebraicGeometry.isOpenImmersion_iff_stalk

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.isEmbedding

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

added theorem AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

modified theorem AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/AlgebraicGeometry/ValuativeCriterion.lean