Commit 2025-10-06 16:30 5b550d3e

View on Github →

chore(AlgebraicGeometry): remove Spec() notation (#30272)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/AlgebraicGeometry/Cover/Open.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

modified def AlgebraicGeometry.coprodSpec

modified def AlgebraicGeometry.sigmaSpec

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

modified theorem AlgebraicGeometry.finite_appTop_of_universallyClosed

modified theorem AlgebraicGeometry.isField_of_universallyClosed

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/PointsPi.lean

modified def AlgebraicGeometry.pointsPi

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

modified def AlgebraicGeometry.Proj.awayι

modified def AlgebraicGeometry.Proj.basicOpenIsoSpec

modified def AlgebraicGeometry.Proj.basicOpenToSpec

modified def AlgebraicGeometry.Proj.toSpecZero

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified theorem AlgebraicGeometry.Scheme.default_asIdeal

Modified Mathlib/AlgebraicGeometry/Stalk.lean

Modified Mathlib/AlgebraicGeometry/ValuativeCriterion.lean