Commit 2023-10-03 07:51 7d196414

View on Github →

feat: some golfing in AlgebraicGeometry.PrimeSpectrum.Basic (#7373)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

modified theorem PrimeSpectrum.isCompact_basicOpen

deleted theorem PrimeSpectrum.punit

Modified Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.isCompactElement_top