Chevalley with complexity bound

Author: YaelDillies

Diff for: Mathlib.lean

@@ -4763,6 +4763,7 @@ import Mathlib.RingTheory.Spectrum.Maximal.Localization
 import Mathlib.RingTheory.Spectrum.Maximal.Topology
 import Mathlib.RingTheory.Spectrum.Prime.Basic
 import Mathlib.RingTheory.Spectrum.Prime.Chevalley
+import Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
 import Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
 import Mathlib.RingTheory.Spectrum.Prime.Defs
 import Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Diff for: Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean

@@ -13,6 +13,11 @@ import Mathlib.RingTheory.Spectrum.Prime.Polynomial
 This file proves Chevalley's theorem, namely that if `f : R → S` is a finitely presented ring hom
 between commutative rings, then the image of a constructible set in `Spec S` is a constructible set
 in `Spec R`.
+
+## See also
+
+`Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` for a version of Chevalley's theorem that
+tracks the degrees and number of polynomials used to construct the constructible sets.
 -/
 
 open Polynomial PrimeSpectrum TensorProduct Topology