Commit 2024-07-24 16:32 cfb75f63

View on Github →

chore: move PartialOrder on PrimeSpectrum to RingTheory. (#15108)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

deleted theorem PrimeSpectrum.asIdeal_le_asIdeal

deleted theorem PrimeSpectrum.asIdeal_lt_asIdeal

Modified Mathlib/RingTheory/PrimeSpectrum.lean

added theorem PrimeSpectrum.asIdeal_le_asIdeal

added theorem PrimeSpectrum.asIdeal_lt_asIdeal

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean