Commit 2025-03-17 19:45 6d9ce960

View on Github →

feat: Chevalley's theorem (#21021) This is https://stacks.math.columbia.edu/tag/00FE. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

added def ChevalleyThm.MvPolynomialC.degBound

added theorem ChevalleyThm.MvPolynomialC.degBound_casesOn_succ

added theorem ChevalleyThm.MvPolynomialC.degBound_le_degBound

added theorem ChevalleyThm.MvPolynomialC.degBound_pos

added theorem ChevalleyThm.MvPolynomialC.degBound_succ

added theorem ChevalleyThm.MvPolynomialC.degBound_zero

added def ChevalleyThm.MvPolynomialC.numBound

added theorem ChevalleyThm.MvPolynomialC.numBound_casesOn_succ

added theorem ChevalleyThm.MvPolynomialC.numBound_mono

added theorem ChevalleyThm.MvPolynomialC.numBound_succ

added theorem ChevalleyThm.MvPolynomialC.numBound_zero

added theorem ChevalleyThm.chevalley_mvPolynomialC

added theorem ChevalleyThm.chevalley_polynomialC

added def ChevalleyThm.degBound

added def ChevalleyThm.numBound

added theorem chevalley_mvPolynomial_mvPolynomial

Modified Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean

added theorem PrimeSpectrum.BasicConstructibleSetData.map_comp'

added theorem PrimeSpectrum.BasicConstructibleSetData.map_comp

added theorem PrimeSpectrum.BasicConstructibleSetData.map_id'

added theorem PrimeSpectrum.BasicConstructibleSetData.map_id

added def PrimeSpectrum.BasicConstructibleSetData.toSet

added theorem PrimeSpectrum.BasicConstructibleSetData.toSet_map

added structure PrimeSpectrum.BasicConstructibleSetData

modified def PrimeSpectrum.ConstructibleSetData.degBound

deleted def PrimeSpectrum.ConstructibleSetData.map

modified theorem PrimeSpectrum.ConstructibleSetData.map_comp

modified theorem PrimeSpectrum.ConstructibleSetData.map_id

modified def PrimeSpectrum.ConstructibleSetData.toSet

modified theorem PrimeSpectrum.ConstructibleSetData.toSet_map