Commit 2023-10-19 18:23 20a9a01a

View on Github →

chore (ValuationSubring): change from set to subtype (#7780) Currently the file uses {S | A ≤ S} for primeSpectrumEquiv and other declarations. This changes those to {S // A ≤ S} which makes the simpNF happier about the generated simp lemmas.

Estimated changes

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

modified def ValuationSubring.primeSpectrumEquiv

modified def ValuationSubring.primeSpectrumOrderEquiv